1.1 --- a/etc/settings	Sun Aug 02 21:03:38 2009 +0200
     1.2 +++ b/etc/settings	Tue Aug 04 01:01:23 2009 +0200
     1.3 @@ -144,6 +144,7 @@
     1.4  # Site settings check -- just to make it a little bit harder to copy this file verbatim!
     1.5  [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
     1.6    { echo >&2 "### Isabelle site settings already present!  Maybe copied etc/settings in full?"; }
     1.7 +ISABELLE_SITE_SETTINGS_PRESENT=true
     1.8  
     1.9  
    1.10  ###