diff -r bd61b838501c -r 4fbdef3e2a55 src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Tue Mar 18 14:05:07 2025 +0100 +++ b/src/Pure/General/ssh.scala Tue Mar 18 19:07:26 2025 +0100 @@ -174,9 +174,9 @@ run_ssh(master = control_master, args = "printenv HOME \";\" printenv SHELL").check.out_lines match { case List(home, shell) => - if (shell.endsWith("/bash")) home + if (shell.endsWith("/bash") || shell.endsWith("/zsh")) home else { - error("Bad SHELL for " + quote(toString) + " -- expected GNU bash, but found " + shell) + error("Bad SHELL for " + quote(toString) + " -- expected bash or zsh, but found " + shell) } case _ => error("Malformed remote environment for " + quote(toString)) }