# HG changeset patch
# User wenzelm
# Date 1476365851 -7200
# Node ID c62b99e3ec07054e0afbb82d13dfaea187d5394f
# Parent  dfb63036c4f63ad3fb0c62ced60903444ece3b53
provide USER_HOME, such that symbolic Path.explode("~") can be used remotely;

diff -r dfb63036c4f6 -r c62b99e3ec07 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)
     }