more robust: Bash.string operations require remote bash;

--- 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)