src/Tools/jEdit/makedist

--- a/src/Tools/jEdit/makedist	Sun Jul 05 17:26:14 2009 +0200
+++ b/src/Tools/jEdit/makedist	Sun Jul 05 17:53:27 2009 +0200
@@ -11,7 +11,7 @@
 
 ## diagnostics
 
-JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre16"
+JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre17"
 
 function usage()
 {
@@ -89,6 +89,7 @@
   print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,; }
   print; }' "$JEDIT/modes/catalog"
 
+
 # build archive
 
 echo "${JEDIT}.tar.gz"