From 070139d3a82ea23e4d050dd5ccebe3f17047cc62 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 30 Jul 2015 08:19:10 +0200
Subject: Fix broken regexp.

Characters do not need to be escaped in character ranges. It just had the
effect of matching backslashes four times.
---
 tools/coq_tex.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 26a9715ef7..8218f84f1f 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -64,8 +64,7 @@ let extract texfile inputv =
  * TeX file [texfile]. The result goes in file [result]. *)
 
 let tex_escaped s =
-  let dollar = "\\$" and  backslash = "\\\\" and expon = "\\^" in
-  let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>'`]") in
+  let delims = Str.regexp "[_{}&%#$\\^~ <>'`]" in
   let adapt_delim = function
     | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
     | "\\" -> "{\\char'134}"
-- 
cgit v1.2.3