# HG changeset patch
# User wenzelm
# Date 1229771863 -3600
# Node ID de921b3cb2639db12d7b4bc033723c4fc4359fed
# Parent  10cdbba5af89904830075dff28b1be2d9b764dc1
updated to 4.3pre16;

diff -r 10cdbba5af89 -r de921b3cb263 src/Tools/jEdit/makedist
--- a/src/Tools/jEdit/makedist	Sat Dec 20 11:07:02 2008 +0100
+++ b/src/Tools/jEdit/makedist	Sat Dec 20 12:17:43 2008 +0100
@@ -11,7 +11,7 @@
 
 ## diagnostics
 
-JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre15"
+JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre16"
 SCALA_HOME="/home/scala/current"
 
 function usage()