more robust: do not assume Bash syntax while testing for it;
authorwenzelm
Wed, 14 Sep 2022 21:14:32 +0200
changeset 76154 dfddb80fc515
parent 76153 bf9f2f4069b9
child 76155 6149f7553ea9
more robust: do not assume Bash syntax while testing for it;
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 {