From 6c683786c8100259e8c78b710e4a75974ae00eba Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Sat, 15 Apr 2017 22:10:08 +0200
Subject: Remove VernacError

---
 ide/texmacspp.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index e787e48bf1..e20704b7fb 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -504,7 +504,6 @@ let rec tmpp v loc =
       xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
                     [tmpp e loc])
   | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
-  | VernacError _ -> xmlWithLoc loc "error" [] []
 
   (* Syntax *)
   | VernacSyntaxExtension (_, ((_, name), sml)) ->
-- 
cgit v1.2.3