# HG changeset patch
# User immler@in.tum.de
# Date 1231605201 -3600
# Node ID 2dd8ced4f2aeb8d1cb4b52d90318a3e5c5b5610f
# Parent  b08299e7bbe620bd1dbb0cac324c8728aa2e4a9d
create folder 'jars' before copying

diff -r b08299e7bbe6 -r 2dd8ced4f2ae 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/"