diff options
| author | Guillaume Melquiond | 2017-09-21 14:10:51 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2017-09-21 14:10:51 +0200 |
| commit | 9c016084a178ebb02f51ffdd2f7cc7c7a98afa4b (patch) | |
| tree | 9c2595a87d85005170ab473762a185da4c1adfce /doc | |
| parent | 88c4a5a2958e2c0bbd2d142e684dc642946e2e41 (diff) | |
Improve support for "-w none" compatibility option.
If coqtop was started with "-w none" yet the script used "Set Warnings
Append", then all the warnings were turned back to their default value.
This commit turns "none" (whatever its sign) into "-all" whenever some
warning status is modified afterward, in order to prevent the issue.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions