equal
deleted
inserted
replaced
22 unset ENV |
22 unset ENV |
23 unset BASH_ENV |
23 unset BASH_ENV |
24 |
24 |
25 #get actual settings |
25 #get actual settings |
26 . $ISABELLE_HOME/etc/settings || exit 2 |
26 . $ISABELLE_HOME/etc/settings || exit 2 |
|
27 ISABELLE_SITE_SETTINGS_PRESENT=true |
27 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings |
28 [ -f $ISABELLE_HOME_USER/etc/settings ] && . $ISABELLE_HOME_USER/etc/settings |
28 |
29 |
29 #append ML system identifier to paths |
30 #append ML system identifier to paths |
30 if [ -z "$ML_PLATFORM" ]; then |
31 if [ -z "$ML_PLATFORM" ]; then |
31 ML_IDENTIFIER="$ML_SYSTEM" |
32 ML_IDENTIFIER="$ML_SYSTEM" |