equal
deleted
inserted
replaced
195 fi |
195 fi |
196 } |
196 } |
197 |
197 |
198 #main components |
198 #main components |
199 init_component "$ISABELLE_HOME" |
199 init_component "$ISABELLE_HOME" |
200 [ -d "$ISABELLE_HOME/doc-src" ] && init_component "$ISABELLE_HOME/doc-src" |
|
201 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin" |
200 [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin" |
202 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" |
201 [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" |
203 |
202 |
204 #ML system identifier |
203 #ML system identifier |
205 if [ -z "$ML_PLATFORM" ]; then |
204 if [ -z "$ML_PLATFORM" ]; then |