# HG changeset patch
# User wenzelm
# Date 1663162944 -7200
# Node ID ccc748255342c2454e5112084b35ec08d3e5cd0a
# Parent  769ebb139a3209ae98315278a2a584613fc12576
more robust: Bash.string operations require remote bash;

diff -r 769ebb139a32 -r ccc748255342 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Sep 14 14:59:01 2022 +0200
+++ b/src/Pure/General/ssh.scala	Wed Sep 14 15:42:24 2022 +0200
@@ -153,7 +153,16 @@
 
     /* init and exit */
 
-    val user_home: String = run_ssh(master = control_master, args = "printenv HOME").check.out
+    val user_home: String =
+      run_ssh(master = control_master, args = "printenv HOME \";\" printenv SHELL").check.out_lines
+      match {
+        case List(user_home, shell) =>
+          if (shell.endsWith("/bash")) user_home
+          else {
+            error("Bad SHELL for " + quote(toString) + " -- expected GNU bash, but found " + shell)
+          }
+        case _ => error("Malformed remote environment for " + quote(toString))
+      }
 
     val settings: JMap[String, String] = JMap.of("HOME", user_home, "USER_HOME", user_home)