diff options
| author | Hendrik Tews | 2021-03-28 22:06:03 +0200 |
|---|---|---|
| committer | Hendrik Tews | 2021-04-12 21:31:12 +0200 |
| commit | e1793962bebf1401026ed961ecc15b7eb60d57f5 (patch) | |
| tree | de4f45d46c7b226fecea6194be5a53b8b648ffbd /doc/plugin_tutorial/README.md | |
| parent | ad34e3a7703d326268bab203864aa84ad3718c2c (diff) | |
[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
Diffstat (limited to 'doc/plugin_tutorial/README.md')
0 files changed, 0 insertions, 0 deletions