diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-28 17:10:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-28 17:10:21 +0200 |
| commit | 6f982439294b9b53150c6c5d2fd1025e58d7bcd9 (patch) | |
| tree | debf9e53d93b722a871364e06763ddc8b0413bcf /stm | |
| parent | 53dc6613499ca18672cda02697f182eb97cda8dc (diff) | |
| parent | 02663c526a3fd347fad803eb664d22e6b5c088ad (diff) | |
Merge branch 'v8.5'
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 |