diff options
Diffstat (limited to 'stm/texmacspp.ml')
| -rw-r--r-- | stm/texmacspp.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 180f20ae8..9edc1f1c7 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -490,6 +490,9 @@ let rec tmpp v loc = | VernacTime l -> xmlApply loc (Element("time",[],[]) :: List.map (fun(loc,e) ->tmpp e loc) l) + | VernacRedirect (s, l) -> + xmlApply loc (Element("redirect",["path", s],[]) :: + List.map (fun(loc,e) ->tmpp e loc) l) | VernacTimeout (s,e) -> xmlApply loc (Element("timeout",["val",string_of_int s],[]) :: [tmpp e loc]) |