equal
deleted
inserted
replaced
142 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" |
142 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" |
143 |
143 |
144 # Site settings check -- just to make it a little bit harder to copy this file verbatim! |
144 # Site settings check -- just to make it a little bit harder to copy this file verbatim! |
145 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ |
145 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ |
146 { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } |
146 { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } |
|
147 ISABELLE_SITE_SETTINGS_PRESENT=true |
147 |
148 |
148 |
149 |
149 ### |
150 ### |
150 ### Default logic |
151 ### Default logic |
151 ### |
152 ### |