# HG changeset patch
# User wenzelm
# Date 1232143224 -3600
# Node ID c787cbe6cdce866a080677df267bb5ac3dff44ea
# Parent  095e5cae6656be980faff2468872862c8ac06ea4# Parent  e561d0915f28ae196788392c6ab5abd166547e9c
merged

diff -r e561d0915f28 -r c787cbe6cdce src/Tools/jEdit/makedist
--- a/src/Tools/jEdit/makedist	Fri Jan 16 22:57:47 2009 +0100
+++ b/src/Tools/jEdit/makedist	Fri Jan 16 23:00:24 2009 +0100
@@ -84,7 +84,7 @@
 
 [ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME"
 cp -R "$JEDIT_HOME/." "$JEDIT/."
-rm -rf "$JEDIT/jEdit"
+rm -rf "$JEDIT/jEdit" "$JEDIT/build-support"
 
 mkdir -p "$JEDIT/jars"