changeset 32305 | c5523ded51d9 |
parent 32292 | ceb7190d7a52 |
child 32332 | bc5cec7b2be6 |
--- a/etc/settings Sun Aug 02 21:03:38 2009 +0200 +++ b/etc/settings Tue Aug 04 01:01:23 2009 +0200 @@ -144,6 +144,7 @@ # Site settings check -- just to make it a little bit harder to copy this file verbatim! [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } +ISABELLE_SITE_SETTINGS_PRESENT=true ###