author | wenzelm |
Thu, 31 Aug 2023 14:59:52 +0200 | |
changeset 78626 | f926602640fe |
parent 78625 | 6aa964f52395 |
child 78627 | fa18208fd7bd |
--- 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>