# HG changeset patch
# User wenzelm
# Date 1335967447 -7200
# Node ID 48b52cdc214ae7abb1efa0cdbbb34481a26ffbd6
# Parent  030d3c89eacf9f8017c98d0a846002796c7f26f6
accomodate scala-2.10.0-M3 with its extra jar;
removed redundant SCALA_JARS;

diff -r 030d3c89eacf -r 48b52cdc214a src/Pure/build-jars
--- 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
 
diff -r 030d3c89eacf -r 48b52cdc214a src/Tools/jEdit/lib/Tools/jedit
--- 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