equal
deleted
inserted
replaced
100 |
100 |
101 #main components |
101 #main components |
102 init_component "$ISABELLE_HOME" |
102 init_component "$ISABELLE_HOME" |
103 |
103 |
104 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \ |
104 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \ |
105 { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER should not be the same directory!"; } |
105 { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER must not be the same directory!"; } |
106 [ -z "$ISABELLE_IGNORE_USER_SETTINGS" -a -f "$ISABELLE_HOME_USER/etc/settings" ] && \ |
106 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" |
107 init_component "$ISABELLE_HOME_USER" |
|
108 |
107 |
109 #ML system identifier |
108 #ML system identifier |
110 if [ -z "$ML_PLATFORM" ]; then |
109 if [ -z "$ML_PLATFORM" ]; then |
111 ML_IDENTIFIER="$ML_SYSTEM" |
110 ML_IDENTIFIER="$ML_SYSTEM" |
112 else |
111 else |