--- a/src/Tools/jEdit/makedist Tue Dec 22 15:42:29 2009 +0100
+++ b/src/Tools/jEdit/makedist Tue Dec 22 17:31:31 2009 +0100
@@ -87,7 +87,7 @@
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-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.info"/>\n\n,; }
+ print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
print; }' "$JEDIT/modes/catalog"