SCALA_HOME: proper line escapes for choosefrom;
authorwenzelm
Fri, 03 Jul 2009 10:54:26 +0200
changeset 31923d6cd15601d8a
parent 31922 d6f8f3bfe329
child 31924 47b59620f37f
child 31936 904f93c76650
SCALA_HOME: proper line escapes for choosefrom;
etc/settings
     1.1 --- a/etc/settings	Fri Jul 03 00:15:59 2009 +0200
     1.2 +++ b/etc/settings	Fri Jul 03 10:54:26 2009 +0200
     1.3 @@ -70,9 +70,10 @@
     1.4  ISABELLE_SCALA="scala"
     1.5  
     1.6  [ -z "$SCALA_HOME" ] && SCALA_HOME=$(choosefrom \
     1.7 -  "$ISABELLE_HOME/contrib/scala"
     1.8 -  "$ISABELLE_HOME/../scala"
     1.9 +  "$ISABELLE_HOME/contrib/scala" \
    1.10 +  "$ISABELLE_HOME/../scala" \
    1.11    "")
    1.12 +
    1.13  [ -n "$SCALA_HOME" ] && ISABELLE_SCALA="$SCALA_HOME/bin/scala"
    1.14  
    1.15  classpath "$ISABELLE_HOME/lib/classes/Pure.jar"