diff options
Diffstat (limited to 'share/man/just-mr-repository-config.5.md')
| -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 05cde2de..1820a0d2 100644 --- a/share/man/just-mr-repository-config.5.md +++ b/share/man/just-mr-repository-config.5.md @@ -184,7 +184,8 @@ part of a Git repository, its Git tree identifier is used; otherwise, the workspace root will be realized as a Git tree in the Git repository in **`just`**'s local build root. -For all workspace roots except *`"distdir"`* the pragma key *`"special"`* is +For all workspace roots except *`"distdir"`*, *`"computed"`*, +and *`"tree structure"`*, the pragma key *`"special"`* is supported. If its value is *`"ignore"`* then it indicates that the workspace root should ignore all special (i.e., neither file, executable, nor tree) entries. For a *`"file"`* workspace root or for an *`"archive"`* workspace root |