From e1793962bebf1401026ed961ecc15b7eb60d57f5 Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Sun, 28 Mar 2021 22:06:03 +0200
Subject: [coqdep] error on non-existent and unreadable files

Print an error message and return non-zero status for
non-existing or unreadable files. Unknown options produce a
warning and are otherwise ignored.
Fixes #14023
---
 man/coqdep.1 | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'man')

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
-- 
cgit v1.2.3