
diff -r 289b92ddb57c -r bbe9ae2c9289 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Mon Oct 12 19:47:29 2015 +0200
+++ b/src/Doc/System/Basics.thy	Mon Oct 12 20:25:08 2015 +0200
@@ -155,7 +155,7 @@
   @{setting HOME}, but on Windows it is the regular home directory of
   the user, not the one of within the Cygwin root
   file-system.\footnote{Cygwin itself offers another choice whether
-  its HOME should point to the \texttt{/home} directory tree or the
+  its HOME should point to the @{file_unchecked "/home"} directory tree or the
   Windows user home.}
 
   \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the




