diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-09-21 14:10:51 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-09-21 14:10:51 +0200 |
| commit | 9c016084a178ebb02f51ffdd2f7cc7c7a98afa4b (patch) | |
| tree | 9c2595a87d85005170ab473762a185da4c1adfce /lib | |
| 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 'lib')
| -rw-r--r-- | lib/cWarnings.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index ff7145267..3699b1c61 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -93,8 +93,12 @@ let split_flags s = "all" flag, and reverses the list. *) let rec cut_before_all_rev acc = function | [] -> acc - | (_status,name as w) :: warnings -> - cut_before_all_rev (w :: if is_all_keyword name then [] else acc) warnings + | (status,name as w) :: warnings -> + let acc = + if is_all_keyword name then [w] + else if is_none_keyword name then [(Disabled,"all")] + else w :: acc in + cut_before_all_rev acc warnings let cut_before_all_rev warnings = cut_before_all_rev [] warnings |