| changeset 34413 | 10cdbba5af89 |
| parent 34395 | 287f3ecdfc2a |
| child 34414 | de921b3cb263 |
--- 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/"