SCALA_HOME: proper line escapes for choosefrom;
authorwenzelm
Fri, 03 Jul 2009 10:54:26 +0200
changeset 31923 d6cd15601d8a
parent 31922 d6f8f3bfe329
child 31924 47b59620f37f
child 31937 904f93c76650
SCALA_HOME: proper line escapes for choosefrom;
etc/settings
--- a/etc/settings	Fri Jul 03 00:15:59 2009 +0200
+++ b/etc/settings	Fri Jul 03 10:54:26 2009 +0200
@@ -70,9 +70,10 @@
 ISABELLE_SCALA="scala"
 
 [ -z "$SCALA_HOME" ] && SCALA_HOME=$(choosefrom \
-  "$ISABELLE_HOME/contrib/scala"
-  "$ISABELLE_HOME/../scala"
+  "$ISABELLE_HOME/contrib/scala" \
+  "$ISABELLE_HOME/../scala" \
   "")
+
 [ -n "$SCALA_HOME" ] && ISABELLE_SCALA="$SCALA_HOME/bin/scala"
 
 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"