equal
deleted
inserted
replaced
19 |
19 |
20 #get actual settings |
20 #get actual settings |
21 . $ISABELLE_HOME/etc/settings || exit 2 |
21 . $ISABELLE_HOME/etc/settings || exit 2 |
22 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings |
22 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings |
23 |
23 |
24 #append ML system to paths |
24 #append ML system identifier to paths |
25 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_SYSTEM" |
25 if [ -z "$ML_PLATFORM" ]; then |
26 ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_SYSTEM; done) |
26 ML_IDENTIFIER="$ML_SYSTEM" |
|
27 else |
|
28 ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
|
29 fi |
|
30 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER" |
|
31 ISABELLE_PATH=$(for DIR in $(echo $ISABELLE_PATH | tr : " "); do echo $DIR/$ML_IDENTIFIER; done) |
27 ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :) |
32 ISABELLE_PATH=$(echo $ISABELLE_PATH | tr " " :) |
28 |
33 |
29 set +o allexport |
34 set +o allexport |