diff options
| author | Maxime Dénès | 2016-11-10 13:24:54 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-14 14:17:11 +0100 |
| commit | 8fe6da32544ee73201f7c64b3dd45afb56c75b71 (patch) | |
| tree | 52c1c123d184fd4d32cc48243245c1012ee5afd5 /toplevel | |
| parent | 30f222b1aad7ec483902b74dfa7dad7aefd5fca3 (diff) | |
Fix bug in warnings: -w foo was silent when foo did not exist.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 5ae1c36ed8..d9f8ed8815 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -524,7 +524,7 @@ let parse_args arglist = |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo |"-toploop" -> set_toploop (next ()) - |"-w" | "-W" -> CWarnings.set_flags (next ()) + |"-w" | "-W" -> CWarnings.set_flags (CWarnings.normalize_flags_string (next ())) |"-o" -> Flags.compilation_output_name := Some (next()) (* Options with zero arg *) |