# HG changeset patch
# User wenzelm
# Date 1261499491 -3600
# Node ID 89fa7e0e8e69db4fe53a9b61f923354a4e3e6cde
# Parent  297a3324944af7c786485c56ee5befe468378947
renamed session.info to session.root;

diff -r 297a3324944a -r 89fa7e0e8e69 src/Tools/jEdit/makedist
--- 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"