# HG changeset patch
# User wenzelm
# Date 1444674308 -7200
# Node ID bbe9ae2c9289c77185903a5a276d8562548cf3db
# Parent  289b92ddb57ccea9161f2e468e988e9ff7bc5c05
clarified antiquotation;

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