equal
deleted
inserted
replaced
150 fi |
150 fi |
151 } |
151 } |
152 |
152 |
153 #main components |
153 #main components |
154 init_component "$ISABELLE_HOME" |
154 init_component "$ISABELLE_HOME" |
155 |
|
156 [ "$ISABELLE_HOME" -ef "$ISABELLE_HOME_USER" ] && \ |
|
157 { echo >&2 "### ISABELLE_HOME and ISABELLE_HOME_USER must not be the same directory!"; } |
|
158 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" |
155 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" |
159 |
156 |
160 #ML system identifier |
157 #ML system identifier |
161 if [ -z "$ML_PLATFORM" ]; then |
158 if [ -z "$ML_PLATFORM" ]; then |
162 ML_IDENTIFIER="$ML_SYSTEM" |
159 ML_IDENTIFIER="$ML_SYSTEM" |