etc/settings
changeset 9225 4772656ddbbc
parent 8880 3a5215883047
child 9236 899b83e8d2e1
--- 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