src/Tools/jEdit/lib/Tools/jedit

   cp -p -R -f "${RESOURCES[@]}" dist/classes/.
   cp src/jEdit.props dist/properties/.
   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,;
       print qq,<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\n\n,;
       print qq,<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n,;