author | immler@in.tum.de |
Sat, 10 Jan 2009 17:33:21 +0100 | |
changeset 34461 | 2dd8ced4f2ae |
parent 34459 | b08299e7bbe6 |
child 34462 | fefbd0421e4e |
--- a/src/Tools/jEdit/makedist Fri Jan 02 15:34:56 2009 +0100 +++ b/src/Tools/jEdit/makedist Sat Jan 10 17:33:21 2009 +0100 @@ -86,6 +86,8 @@ cp -R "$JEDIT_HOME/." "$JEDIT/." rm -rf "$JEDIT/jEdit" +mkdir "$JEDIT/jars" + [ "$SCALA_HOME/lib/scala-library.jar" ] || fail "Bad Scala directory: $SCALA_HOME" cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/"