# HG changeset patch
# User wenzelm
# Date 1663182872 -7200
# Node ID dfddb80fc5154b221ff80058ab24e29041d18467
# Parent  bf9f2f4069b90931f18dd03a4930e9b984675fac
more robust: do not assume Bash syntax while testing for it;

diff -r bf9f2f4069b9 -r dfddb80fc515 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Wed Sep 14 17:35:38 2022 +0200
+++ b/src/Pure/General/ssh.scala	Wed Sep 14 21:14:32 2022 +0200
@@ -155,8 +155,8 @@
     /* init and exit */
 
     val user_home: String = {
-      val args = Bash.string("printenv HOME\nprintenv SHELL")
-      run_ssh(master = control_master, args = args).check.out_lines match {
+      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 {