# HG changeset patch
# User wenzelm
# Date 1294773528 -3600
# Node ID 917f1a4fbc7784815267fa00c65bd562020dbec3
# Parent  0ffd5ea44078ebe9843e895c0069ec08790d20e1
added dist/jedit symlink for convenience;

diff -r 0ffd5ea44078 -r 917f1a4fbc77 src/Tools/jEdit/makedist
--- a/src/Tools/jEdit/makedist	Tue Jan 11 20:10:34 2011 +0100
+++ b/src/Tools/jEdit/makedist	Tue Jan 11 20:18:48 2011 +0100
@@ -74,6 +74,8 @@
 rm -rf "$JEDIT" jedit
 mkdir "$JEDIT"
 
+rm -f jedit && ln -s "$JEDIT" jedit
+
 
 # copy stuff