# HG changeset patch
# User wenzelm
# Date 1693486792 -7200
# Node ID f926602640feb97c29c0d77b135ea7cdd84c6029
# Parent  6aa964f52395f849ca18b01f1b8d74503a8af508
more portable: it really is the Cygwin $HOME not the Windows $USER_HOME;

diff -r 6aa964f52395 -r f926602640fe src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed Aug 30 17:02:40 2023 +0200
+++ b/src/Doc/System/Sessions.thy	Thu Aug 31 14:59:52 2023 +0200
@@ -530,7 +530,7 @@
   such as @{system_option "build_database_server"}, @{system_option
   "build_database_host"}, or @{system_option "build_database_ssh_host"}.
   Remote host connections are managed via regular SSH configuration, see also
-  \<^path>\<open>$HOME/.ssh/config\<close> on each node.
+  \<^verbatim>\<open>$HOME/.ssh/config\<close> on each node.
 \<close>