diff options
| author | coqbot-app[bot] | 2021-04-13 14:10:33 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-13 14:10:33 +0000 |
| commit | ea62d1e19f2ba565ea3a18ba3709a06af5c845ac (patch) | |
| tree | 3193f7dafa0fc93c1c9b3fc8d47fcc1c2c075f6e /man | |
| parent | b78e6cfcb412d1c4e5902fb895c5ecaa0cb177ac (diff) | |
| parent | e1793962bebf1401026ed961ecc15b7eb60d57f5 (diff) | |
Merge PR #14024: [coqdep] error on non-existent and unreadable files
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: ejgallego
Diffstat (limited to 'man')
| -rw-r--r-- | man/coqdep.1 | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/man/coqdep.1 b/man/coqdep.1 index bb6b20c0bb..5ca558b7c5 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -70,6 +70,21 @@ Output dependencies for .vos files (this is not the default as it breaks dune's .B \-boot For coq developers, prints dependencies over coq library files (omitted by default). +.TP +.B \-noinit +Currently no effect. + + +.SH EXIT STATUS +.IP "1" +A file given on the command line cannot be found or some file +cannot be opened. +.IP "0" +In all other cases. In particular, when a dependency cannot be +found or an invalid option is encountered, +.B coqdep +prints a warning and exits with status +.B 0\fR. .SH SEE ALSO |