equal
deleted
inserted
replaced
97 ML_IDENTIFIER="$ML_SYSTEM" |
97 ML_IDENTIFIER="$ML_SYSTEM" |
98 else |
98 else |
99 ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
99 ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
100 fi |
100 fi |
101 |
101 |
102 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" |
|
103 |
|
104 #enforce JAVA_HOME |
102 #enforce JAVA_HOME |
105 if [ -d "$ISABELLE_JDK_HOME/jre" ] |
103 if [ -d "$ISABELLE_JDK_HOME/jre" ] |
106 then |
104 then |
107 export JAVA_HOME="$ISABELLE_JDK_HOME/jre" |
105 export JAVA_HOME="$ISABELLE_JDK_HOME/jre" |
108 else |
106 else |