diff options
| author | Oliver Reiche <oliver.reiche@huawei.com> | 2024-03-06 16:49:28 +0100 |
|---|---|---|
| committer | Oliver Reiche <oliver.reiche@huawei.com> | 2024-03-08 14:18:43 +0100 |
| commit | ef15067da1e1615029d1a7ef835bb5278bc81c8d (patch) | |
| tree | 23cc12b1fb2564cfd3cee6f42f5444f66925e6f8 /share | |
| parent | a2ffc06b03cdaf013ddf8825d60b8ee4a9dca431 (diff) | |
| download | justbuild-ef15067da1e1615029d1a7ef835bb5278bc81c8d.tar.gz | |
doc: Update man page on Git file URLs
Diffstat (limited to 'share')
| -rw-r--r-- | share/man/just-mr-repository-config.5.md | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/share/man/just-mr-repository-config.5.md b/share/man/just-mr-repository-config.5.md index 97901061..90ae5055 100644 --- a/share/man/just-mr-repository-config.5.md +++ b/share/man/just-mr-repository-config.5.md @@ -100,7 +100,8 @@ It defines as workspace root a part of a Git repository. The following fields are supported: - *`"repository"`* provides the URL of the Git repository. This entry - is mandatory. + is mandatory. Note that only URLs starting with `/`, `./`, or `file://` + are considered file URLs. - *`"commit"`* contains the commit hash. This has to be specified in hex encoding. This entry is mandatory. |