equal
deleted
inserted
replaced
85 splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}") |
85 splitarray ":" "$ISABELLE_COMPONENTS"; declare -a AVAILABLE_COMPONENTS=("${SPLITARRAY[@]}") |
86 splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}") |
86 splitarray ":" "$ISABELLE_COMPONENTS_MISSING"; declare -a MISSING_COMPONENTS=("${SPLITARRAY[@]}") |
87 |
87 |
88 if [ -n "$INIT_SETTINGS" ]; then |
88 if [ -n "$INIT_SETTINGS" ]; then |
89 SETTINGS="$ISABELLE_HOME_USER/etc/settings" |
89 SETTINGS="$ISABELLE_HOME_USER/etc/settings" |
90 SETTINGS_CONTENT='init_components "$USER_HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"' |
90 SETTINGS_CONTENT='init_components "$ISABELLE_COMPONENTS_BASE" "$ISABELLE_HOME/Admin/components/main"' |
91 if [ -e "$SETTINGS" ]; then |
91 if [ -e "$SETTINGS" ]; then |
92 echo "User settings file already exists!" |
92 echo "User settings file already exists!" |
93 echo |
93 echo |
94 echo "Edit \"$SETTINGS\" manually" |
94 echo "Edit \"$SETTINGS\" manually" |
95 echo "and add the following line near its start:" |
95 echo "and add the following line near its start:" |