diff options
| author | Paul Cristian Sarbu <paul.cristian.sarbu@huawei.com> | 2023-02-27 14:27:10 +0100 |
|---|---|---|
| committer | Paul Cristian Sarbu <paul.cristian.sarbu@huawei.com> | 2023-03-08 12:22:15 +0100 |
| commit | 94c180ea2ded808c749e69ad36757ce1d390711a (patch) | |
| tree | 94aee1621a1f69c4464b77a5d8961612b6efe592 /share | |
| parent | f4ce0e45981df58ebb10806d53b82beb90a596ce (diff) | |
| download | justbuild-94c180ea2ded808c749e69ad36757ce1d390711a.tar.gz | |
docs: Update just-mr section-5 man page with new 'git tree' repository type
Diffstat (limited to 'share')
| -rw-r--r-- | share/man/just-mr-repository-config.5.org | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/share/man/just-mr-repository-config.5.org b/share/man/just-mr-repository-config.5.org index 87fdd9d7..2210aa76 100644 --- a/share/man/just-mr-repository-config.5.org +++ b/share/man/just-mr-repository-config.5.org @@ -85,6 +85,23 @@ The following fields are supported: This entry is optional. If missing, the root directory of the Git repository is used. +*** ~"git tree"~ + +It defines as workspace root a known Git tree obtainable by a generic command. + +The following fields are supported: + +- ~"id"~ provides the Git tree identifier. + This entry is mandatory. + +- ~"cmd"~ provides a list of strings forming a command which promises that, when + executed in an empty directory (anywhere in the file system), creates in that + directory a directory structure containing the promised Git tree (either + top-level or in some subdirectory). + This entry is mandatory. + +- ~"env"~ provides a map of envariables to be set for executing the command. + *** ~"distdir"~ It defines as workspace root a directory with the distribution archives |