# HG changeset patch
# User wenzelm
# Date 1742322914 -3600
# Node ID 332afbd48bcf5d957e6cb6964c64d7be6c09ae53
# Parent  d546eb3454267842f0d08904ab18393e312afea4# Parent  4fbdef3e2a5558813c4c4c5949e038dc780720d5
merged

diff -r d546eb345426 -r 332afbd48bcf NEWS
--- a/NEWS	Tue Mar 18 18:12:07 2025 +0000
+++ b/NEWS	Tue Mar 18 19:35:14 2025 +0100
@@ -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)
 --------------------------------
diff -r d546eb345426 -r 332afbd48bcf src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Tue Mar 18 18:12:07 2025 +0000
+++ b/src/Pure/General/ssh.scala	Tue Mar 18 19:35:14 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))
       }