removed jEdit sources from target;
authorwenzelm
Sat, 20 Dec 2008 11:07:02 +0100
changeset 34413 10cdbba5af89
parent 34412 c60770179a0c
child 34414 de921b3cb263
removed jEdit sources from target;
src/Tools/jEdit/makedist
--- a/src/Tools/jEdit/makedist	Sat Dec 20 00:14:25 2008 +0100
+++ b/src/Tools/jEdit/makedist	Sat Dec 20 11:07:02 2008 +0100
@@ -84,6 +84,7 @@
 
 [ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME"
 cp -R "$JEDIT_HOME/." "$JEDIT/."
+rm -rf "$JEDIT/jEdit"
 
 [ "$SCALA_HOME/lib/scala-library.jar" ] || fail "Bad Scala directory: $SCALA_HOME"
 cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/"