From 9060a941d8b7566220f6fb6a191ac2fd7eca7315 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 17 Sep 2014 17:17:53 +0200
Subject: Remove pointless regex for '""' as the empty string already matches
 it.

---
 ide/coq.lang | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/ide/coq.lang b/ide/coq.lang
index 7679f863d9..608a4aeaea 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -55,7 +55,6 @@
 	  <include>
 	    <context ref="comment-in-comment"/>
 	    <context ref="string"/>
-	    <context ref="escape-seq"/>
 	  </include>
 	</context>
 	<context id="comment" style-ref="comment" class="comment" class-disabled="no-spell-check">
@@ -68,11 +67,9 @@
 	      <include>
 		<context ref="comment-in-comment"/>
 		<context ref="string"/>
-		<context ref="escape-seq"/>
 	      </include>
 	    </context>
 	    <context ref="string"/>
-	    <context ref="escape-seq"/>
 	  </include>
 	</context>
 	<context id="declaration">
-- 
cgit v1.2.3