diff -r 0da360494917 -r 4772656ddbbc etc/settings
--- a/etc/settings	Sat Jul 01 19:48:04 2000 +0200
+++ b/etc/settings	Sat Jul 01 19:49:09 2000 +0200
@@ -2,7 +2,7 @@
 # $Id$
 #
 # Isabelle settings -- site defaults.
-# Do *NOT* copy this file into your personal isabelle directory!
+# Do *NOT* copy this file into your personal isabelle directory!!!
 
 ###
 ### ML compiler settings (ESSENTIAL!)
@@ -93,6 +93,10 @@
   ISABELLE_BROWSER_INFO=$ISABELLE_HOME_USER/browser_info
 fi
 
+# Site settings check -- just to make it a little bit harder to copy this file!
+[ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
+  { echo >&2 "### Isabelle site settings already present!  Maybe copied etc/settings in full?"; }
+
 #Users may want to change this.
 ISABELLE_LOGIC=HOL