diff options
| author | Maxime Dénès | 2017-10-05 19:41:32 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-05 19:41:32 +0200 |
| commit | 2aac4ae818fec0d409da31ef9da83796d871d687 (patch) | |
| tree | f01c726982850aace7761a79324abeee775482ea | |
| parent | 9c033b4da738fb399eebe9f8ccf0f8a407d6d42e (diff) | |
| parent | 9c016084a178ebb02f51ffdd2f7cc7c7a98afa4b (diff) | |
Merge PR #1069: Improve support for -w options
| -rw-r--r-- | lib/cWarnings.ml | 8 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 7 |
2 files changed, 12 insertions, 3 deletions
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index ff71452672..3699b1c614 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 diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c1cdaa5a34..db7bcb76b1 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -539,7 +539,12 @@ let parse_args arglist = |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Flags.Vio2Vo |"-toploop" -> set_toploop (next ()) - |"-w" | "-W" -> CWarnings.set_flags (CWarnings.normalize_flags_string (next ())) + |"-w" | "-W" -> + let w = next () in + if w = "none" then CWarnings.set_flags w + else + let w = CWarnings.get_flags () ^ "," ^ w in + CWarnings.set_flags (CWarnings.normalize_flags_string w) |"-o" -> Flags.compilation_output_name := Some (next()) (* Options with zero arg *) |