diff options
| -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 a641c37f..b9d5c5cd 100644 --- a/share/man/just-mr-repository-config.5.md +++ b/share/man/just-mr-repository-config.5.md @@ -217,7 +217,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 |