equal
deleted
inserted
replaced
76 ISABELLE_IDENTIFIER="$(cat "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER")" |
76 ISABELLE_IDENTIFIER="$(cat "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER")" |
77 fi |
77 fi |
78 |
78 |
79 ISABELLE_NAME="${ISABELLE_IDENTIFIER:-Isabelle}" |
79 ISABELLE_NAME="${ISABELLE_IDENTIFIER:-Isabelle}" |
80 |
80 |
|
81 ISABELLE_HOSTNAME="$(hostname -s)" |
|
82 |
81 |
83 |
82 # components |
84 # components |
83 |
85 |
84 ISABELLE_COMPONENTS="" |
86 ISABELLE_COMPONENTS="" |
85 ISABELLE_COMPONENTS_MISSING="" |
87 ISABELLE_COMPONENTS_MISSING="" |