diff options
| author | Emilio Jesus Gallego Arias | 2016-11-16 10:51:39 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-11-17 10:14:40 +0100 |
| commit | 26d180fa0b27edc773fd07c73906e4ed56475200 (patch) | |
| tree | 7b79952cd7221013f444dfdf8b3b9732be8365a1 /ide | |
| parent | 3a51aa7265f35dd3cbf3f7bff858d663e4406146 (diff) | |
[stm] Remove STM-related vernaculars
I think these commands never make a lot of sense on scripts other than
debugging and we have better methods now.
The last remaining command, used for the tty emulation has been renamed
to VtBack, but it should go away at some point too once the legacy
interfaces are removed.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/texmacspp.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 680da7f54b..dbcd8630b1 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -724,9 +724,6 @@ let rec tmpp v loc = | VernacComments (cl) -> xmlComment loc (List.flatten (List.map pp_comment cl)) - (* Stm backdoor *) - | VernacStm _ as x -> xmlTODO loc x - (* Proof management *) | VernacGoal _ as x -> xmlTODO loc x | VernacAbort _ as x -> xmlTODO loc x |