From b3dbd589e1dc41d7bce18afd87dd6e59968286bb Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 30 Sep 2016 22:50:49 +0200
Subject: Add command 'Set foo Append "bar"' for appending to an option (bug
 #5109).

For now, the only meaningful user is "Set Warnings". Example:

Section Bar.
  Local Set Warnings Append "-foo".
  (* warning foo is now disabled *)
End Bar.
(* foo is now reenabled, assuming it was before entering the section *)
---
 parsing/g_vernac.ml4 | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 50e469dd2a..96eede2b96 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -851,6 +851,8 @@ GEXTEND Gram
       (* For acting on parameter tables *)
       | "Set"; table = option_table; v = option_value ->
   	  VernacSetOption (table,v)
+      | "Set"; table = option_table; "Append"; v = STRING ->
+         VernacSetAppendOption (table,v)
       | "Set"; table = option_table ->
   	  VernacSetOption (table,BoolValue true)
       | IDENT "Unset"; table = option_table ->
-- 
cgit v1.2.3