# HG changeset patch
# User wenzelm
# Date 1443734791 -7200
# Node ID 12378df46752af0a72a5620bf8fe97287945f45f
# Parent  754e8ddbbc82e47addbac4fc873179643156584d
less ambitious regex -- avoid unclarities of escaping;

diff -r 754e8ddbbc82 -r 12378df46752 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Oct 01 18:59:53 2015 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Oct 01 23:26:31 2015 +0200
@@ -295,7 +295,7 @@
   cp -p -R -f src/modes/. dist/modes/.
 
   perl -i -e 'while (<>) {
-    if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="\*\.{sml,ml}"/) { }
+    if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="...sml,ml."/) { }
     elsif (m/NAME="javacc"/) {
       print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
       print qq,<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n,;