--- a/src/Pure/build-jars Wed May 02 13:09:26 2012 +0200
+++ b/src/Pure/build-jars Wed May 02 16:04:07 2012 +0200
@@ -200,6 +200,8 @@
fail "Failed to produce $TARGET"
cp "$SCALA_HOME/lib/scala-swing.jar" "$SCALA_HOME/lib/scala-library.jar" "$TARGET_DIR/ext"
+ [ -e "$SCALA_HOME/lib/scala-actors.jar" ] && \
+ cp "$SCALA_HOME/lib/scala-actors.jar" "$TARGET_DIR/ext"
popd >/dev/null
--- a/src/Tools/jEdit/lib/Tools/jedit Wed May 02 13:09:26 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed May 02 16:04:07 2012 +0200
@@ -167,12 +167,6 @@
"$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
)
-SCALA_JARS=(
- "$SCALA_HOME/lib/scala-compiler.jar"
- "$SCALA_HOME/lib/scala-library.jar"
- "$SCALA_HOME/lib/scala-swing.jar"
-)
-
# target