diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-11-03 17:55:37 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-11-03 17:55:37 +0100 |
| commit | 0c01a177362f8d7408ba8906fe0cba1948d8fb9c (patch) | |
| tree | ee84a305e691da2d6c87eb830c4b94376f2f19e1 /parsing/g_vernac.ml4 | |
| parent | df1720bff67889818f8b4856f29ac02540d7f756 (diff) | |
| parent | 2c5eef988f11979175de6d1983bc533ce18b1095 (diff) | |
Merge remote-tracking branch 'github/pr/340' into v8.6
Was PR#340: Fix various shortcomings of the warnings infrastructure.
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 5e2856b2f..8f86abcf3 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -876,11 +876,16 @@ GEXTEND Gram | "Set"; table = option_table; v = option_value -> begin match v with | StringValue s -> - let (last, prefix) = List.sep_last table in - if String.equal last "Append" && not (List.is_empty prefix) then - VernacSetAppendOption (prefix, s) + (* We make a special case for warnings because appending is their + natural semantics *) + if CString.List.equal table ["Warnings"] then + VernacSetAppendOption (table, s) else - VernacSetOption (table, v) + let (last, prefix) = List.sep_last table in + if String.equal last "Append" && not (List.is_empty prefix) then + VernacSetAppendOption (prefix, s) + else + VernacSetOption (table, v) | _ -> VernacSetOption (table, v) end | "Set"; table = option_table -> |