diff options
| author | Paul Cristian Sarbu <paul.cristian.sarbu@huawei.com> | 2023-11-10 11:53:45 +0100 |
|---|---|---|
| committer | Paul Cristian Sarbu <paul.cristian.sarbu@huawei.com> | 2023-11-14 13:35:01 +0100 |
| commit | a987adcbb97f878698018c1ec73536ad9bc2dcac (patch) | |
| tree | 464e22e2d07c0f68873249364e4ac4d016cdf29f /share/man/just-import-git.1.md | |
| parent | 2e54838fae527baba13d88e505f3e4241c45a3a8 (diff) | |
| download | justbuild-a987adcbb97f878698018c1ec73536ad9bc2dcac.tar.gz | |
man: Add documentation for specifying alternative mirrors
Diffstat (limited to 'share/man/just-import-git.1.md')
| -rw-r--r-- | share/man/just-import-git.1.md | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/share/man/just-import-git.1.md b/share/man/just-import-git.1.md index def3e495..4d33f488 100644 --- a/share/man/just-import-git.1.md +++ b/share/man/just-import-git.1.md @@ -82,6 +82,14 @@ for a single repository. Useful, if the repository to be imported does not have a repository configuration or should be imported without dependencies. +**`--mirror`** *`URL`* +Provides an alternative fetch location for the imported repository. +Specifying this option multiple times will accumulate URLs in the order +they appear on the command line. These URLs will not be used during the +import, but instead will be recorded as the value of the `"mirrors"` key +in the resulting configuration of the imported repository. +See **`just-mr-repository-config`**(5). + See also ======== |