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 /doc | |
| 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 'doc')
| -rw-r--r-- | doc/changelog/08-cli-tools/14024-coqdep-errors.rst | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/changelog/08-cli-tools/14024-coqdep-errors.rst b/doc/changelog/08-cli-tools/14024-coqdep-errors.rst new file mode 100644 index 0000000000..355c0bd7b7 --- /dev/null +++ b/doc/changelog/08-cli-tools/14024-coqdep-errors.rst @@ -0,0 +1,8 @@ +- **Changed:** + ``coqdep`` now reports an error if files specified on the + command line don't exist or if it encounters unreadable files. + Unknown options now generate a warning. Previously these + conditions were ignored. + (`#14024 <https://github.com/coq/coq/pull/14024>`_, + fixes `#14023 <https://github.com/coq/coq/issues/14023>`_, + by Hendrik Tews). |