diff -r 5f25eb86c6a0 -r 30e49efdd4e3 src/Tools/jEdit/makedist --- a/src/Tools/jEdit/makedist Sat Dec 20 14:48:10 2008 +0100 +++ b/src/Tools/jEdit/makedist Sat Dec 20 16:04:17 2008 +0100 @@ -91,6 +91,10 @@ cp -R "$THIS/dist-template/." "$JEDIT/." +perl -i -e 'while (<>) { if (m/NAME="javacc"/) { + print qq,\n\n,; } + print; }' "$JEDIT/modes/catalog" + cp jars/Isabelle-jEdit.jar "$JEDIT/jars/isabelle.jar" cp jars/lib/Pure.jar "$JEDIT/jars/isabelle-Pure.jar" cp jars/lib/core-renderer.jar "$JEDIT/jars/"