equal
deleted
inserted
replaced
53 |
53 |
54 ### |
54 ### |
55 ### JVM components (Scala or Java) |
55 ### JVM components (Scala or Java) |
56 ### |
56 ### |
57 |
57 |
58 ISABELLE_JAVA="${THIS_JAVA:-java}" |
58 ISABELLE_JAVA="java" |
59 ISABELLE_SCALA="scala" |
59 ISABELLE_SCALA="scala" |
60 |
60 |
61 [ -z "$SCALA_HOME" ] && SCALA_HOME=$(choosefrom \ |
61 [ -z "$SCALA_HOME" ] && SCALA_HOME=$(choosefrom \ |
62 "$ISABELLE_HOME/contrib/scala" \ |
62 "$ISABELLE_HOME/contrib/scala" \ |
63 "$ISABELLE_HOME/../scala" \ |
63 "$ISABELLE_HOME/../scala" \ |