# 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