etc/settings

--- 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
 
 
 ###