src/Tools/jEdit/makedist
changeset 34461 2dd8ced4f2ae
parent 34419 30e49efdd4e3
child 34469 bd813e4e97d3
--- 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/"