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 *) --- ide/texmacspp.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'ide') diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 9de1df9f1..680da7f54 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -709,6 +709,7 @@ let rec tmpp v loc = | VernacSetStrategy _ as x -> xmlTODO loc x | VernacUnsetOption _ as x -> xmlTODO loc x | VernacSetOption _ as x -> xmlTODO loc x + | VernacSetAppendOption _ as x -> xmlTODO loc x | VernacAddOption _ as x -> xmlTODO loc x | VernacRemoveOption _ as x -> xmlTODO loc x | VernacMemOption _ as x -> xmlTODO loc x -- cgit v1.2.3