Merge pull request #68524 from nspin/pr/repo-manifest-name

fetchRepoProject: add manifestName parameter
This commit is contained in:
Jörg Thalheim 2020-08-14 20:08:25 +01:00 committed by GitHub
commit 1f2c19f158
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -2,7 +2,7 @@
{ name, manifest, rev ? "HEAD", sha256
# Optional parameters:
, repoRepoURL ? "", repoRepoRev ? "", referenceDir ? ""
, repoRepoURL ? "", repoRepoRev ? "", referenceDir ? "", manifestName ? ""
, localManifests ? [], createMirror ? false, useArchive ? false
}:
@ -16,6 +16,7 @@ let
(optionalString (repoRepoURL != "") "--repo-url=${repoRepoURL}")
(optionalString (repoRepoRev != "") "--repo-branch=${repoRepoRev}")
(optionalString (referenceDir != "") "--reference=${referenceDir}")
(optionalString (manifestName != "") "--manifest-name=${manifestName}")
];
repoInitFlags = [