provide USER_HOME, such that symbolic Path.explode("~") can be used remotely;
authorwenzelm
Thu, 13 Oct 2016 15:37:31 +0200
changeset 64190 c62b99e3ec07
parent 64189 dfb63036c4f6
child 64191 1dcb5acd9a71
provide USER_HOME, such that symbolic Path.explode("~") can be used remotely;
src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Thu Oct 13 15:17:10 2016 +0200
+++ b/src/Pure/General/ssh.scala	Thu Oct 13 15:37:31 2016 +0200
@@ -288,7 +288,7 @@
     {
       val kind = "exec"
       val channel = session.openChannel(kind).asInstanceOf[ChannelExec]
-      channel.setCommand(command)
+      channel.setCommand("export USER_HOME=\"$HOME\"\n" + command)
       new Exec(this, kind, channel)
     }