diff options
Diffstat (limited to 'ide/texmacspp.ml')
| -rw-r--r-- | ide/texmacspp.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 9890a518c..6fbed38fb 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -705,6 +705,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 |