# 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>\$HOME/.ssh/config\ on each node. + \<^verbatim>\$HOME/.ssh/config\ on each node. \