--- a/NEWS Tue Mar 18 21:39:29 2025 +0000
+++ b/NEWS Tue Mar 18 21:39:42 2025 +0000
@@ -110,6 +110,12 @@
* Removed theory "HOL-Library.Divides" (finally).
+*** System ***
+
+* SSH connections allow both bash and zsh as remote shell. This is
+particularly important for macOS, where zsh is the default user shell.
+
+
New in Isabelle2025 (March 2025)
--------------------------------
--- a/src/Pure/General/ssh.scala Tue Mar 18 21:39:29 2025 +0000
+++ b/src/Pure/General/ssh.scala Tue Mar 18 21:39:42 2025 +0000
@@ -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))
}