# HG changeset patch
# User wenzelm
# Date 1389033772 -3600
# Node ID ce4bf91331e7802e18080cb9d4aaefc749063abd
# Parent  30e2503f1aa2742567bd2900d9e64bff0ed0f383
misc tuning and clarification;

diff -r 30e2503f1aa2 -r ce4bf91331e7 etc/settings
--- a/etc/settings	Mon Jan 06 17:47:44 2014 +0100
+++ b/etc/settings	Mon Jan 06 19:42:52 2014 +0100
@@ -1,11 +1,12 @@
 # -*- shell-script -*- :mode=shellscript:
 #
-# Isabelle settings -- distribution defaults.
+# Isabelle system settings.
 #
 # Important notes:
 #   * See the "system" manual for explanations on Isabelle settings
+#   * User settings go into $ISABELLE_HOME_USER/etc/settings
 #   * DO NOT EDIT the repository copy of this file!
-#   * DO NOT COPY this file into your $ISABELLE_HOME_USER directory!
+#   * DO NOT COPY this file into the $ISABELLE_HOME_USER directory!
 
 ###
 ### Isabelle/Scala
diff -r 30e2503f1aa2 -r ce4bf91331e7 etc/user-settings.sample
--- a/etc/user-settings.sample	Mon Jan 06 17:47:44 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-#
-# Isabelle user settings sample -- for use in $ISABELLE_HOME_USER/etc/settings
-
-ISABELLE_BUILD_OPTIONS="browser_info document=pdf"
-ISABELLE_LOGIC=HOL
diff -r 30e2503f1aa2 -r ce4bf91331e7 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Mon Jan 06 17:47:44 2014 +0100
+++ b/src/Doc/System/Basics.thy	Mon Jan 06 19:42:52 2014 +0100
@@ -101,14 +101,10 @@
   before --- usually to something like @{verbatim
   "$USER_HOME/.isabelle/IsabelleXXXX"}.
   
-  Thus individual users may override the site-wide defaults.  See also
-  file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the
-  distribution.  Typically, a user settings file would contain only a
-  few lines, just the assigments that are really changed.  One should
-  definitely \emph{not} start with a full copy the basic @{file
-  "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
-  maintainance problems later, when the Isabelle installation is
-  updated or changed otherwise.
+  Thus individual users may override the site-wide defaults.
+  Typically, a user settings file contains only a few lines, with some
+  assignments that are actually changed.  Never copy the central
+  @{file "$ISABELLE_HOME/etc/settings"} file!
   
   \end{enumerate}