suppress "FreeMarker Template Language" file extension for the sake of SAD3/ForTheL;
authorwenzelm
Sun, 28 Oct 2018 14:00:51 +0100
changeset 69202 e0c32187916b
parent 69201 0b61266fc2e0
child 69203 a5c0d61ce5db
suppress "FreeMarker Template Language" file extension for the sake of SAD3/ForTheL;
src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sun Oct 28 11:00:09 2018 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Oct 28 14:00:51 2018 +0100
@@ -373,7 +373,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."/ or m/FILE_NAME_GLOB="..ftl"/) { }
     elsif (m/NAME="javacc"/) {
       print qq!<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>\n\n!;
       print qq!<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n!;