--- a/src/Tools/jEdit/makedist Mon Dec 21 21:49:43 2009 +0100
+++ b/src/Tools/jEdit/makedist Mon Dec 21 21:50:30 2009 +0100
@@ -86,7 +86,8 @@
cp -R "$THIS/dist-template/." "$JEDIT/."
perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
- print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,; }
+ print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
+ print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.info"/>\n\n,; }
print; }' "$JEDIT/modes/catalog"