# HG changeset patch
# User wenzelm
# Date 1510411927 -3600
# Node ID 3d81a1a6730280380be4f7fa1f4728d82f8ec426
# Parent  848672fcaee58bdd6c38ce45f0284084d3c7fd14
tuned;

diff -r 848672fcaee5 -r 3d81a1a67302 src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Sat Nov 11 15:45:12 2017 +0100
+++ b/src/Doc/System/Environment.thy	Sat Nov 11 15:52:07 2017 +0100
@@ -58,7 +58,7 @@
     \<^enum> The file @{path "$ISABELLE_HOME_USER/etc/settings"} (if it
     exists) is run in the same way as the site default settings. Note that the
     variable @{setting ISABELLE_HOME_USER} has already been set before ---
-    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
+    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2017\<close>.
 
     Thus individual users may override the site-wide defaults. Typically, a
     user settings file contains only a few lines, with some assignments that