create folder 'jars' before copying
authorimmler@in.tum.de
Sat, 10 Jan 2009 17:33:21 +0100
changeset 34461 2dd8ced4f2ae
parent 34459 b08299e7bbe6
child 34462 fefbd0421e4e
create folder 'jars' before copying
src/Tools/jEdit/makedist
--- 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/"