equal
deleted
inserted
replaced
45 source "$ISABELLE_HOME/etc/settings" || exit 2 |
45 source "$ISABELLE_HOME/etc/settings" || exit 2 |
46 ISABELLE_SITE_SETTINGS_PRESENT=true |
46 ISABELLE_SITE_SETTINGS_PRESENT=true |
47 |
47 |
48 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \ |
48 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \ |
49 { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; } |
49 { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; } |
50 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && source "$ISABELLE_HOME_USER/etc/settings" |
50 [ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \ |
|
51 source "$ISABELLE_HOME_USER/etc/settings" || exit 2 |
51 |
52 |
52 #append ML system identifier to paths |
53 #append ML system identifier to paths |
53 if [ -z "$ML_PLATFORM" ]; then |
54 if [ -z "$ML_PLATFORM" ]; then |
54 ML_IDENTIFIER="$ML_SYSTEM" |
55 ML_IDENTIFIER="$ML_SYSTEM" |
55 else |
56 else |