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