author | wenzelm |
Sun, 11 Jan 2009 19:33:53 +0100 | |
changeset 34469 | bd813e4e97d3 |
parent 34468 | 9d4b4f290676 |
child 34470 | f4c033b33630 |
--- a/src/Tools/jEdit/makedist Sun Jan 11 19:32:26 2009 +0100 +++ b/src/Tools/jEdit/makedist Sun Jan 11 19:33:53 2009 +0100 @@ -86,7 +86,7 @@ cp -R "$JEDIT_HOME/." "$JEDIT/." rm -rf "$JEDIT/jEdit" -mkdir "$JEDIT/jars" +mkdir -p "$JEDIT/jars" [ "$SCALA_HOME/lib/scala-library.jar" ] || fail "Bad Scala directory: $SCALA_HOME" cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/"