diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/texmacspp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 9edc1f1c7..aaa6c2c07 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -509,8 +509,10 @@ let rec tmpp v loc = | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name [] | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name [] - | VernacDelimiters (name,tag) -> + | VernacDelimiters (name,Some tag) -> xmlScope loc "delimit" name ~attr:["delimiter",tag] [] + | VernacDelimiters (name,None) -> + xmlScope loc "undelimit" name ~attr:[] [] | VernacBindScope (name,l) -> xmlScope loc "bind" name (List.map (function |