less ambitious regex -- avoid unclarities of escaping;

--- 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,;