src/Pure/Admin/remote_dmg.scala
Mon, 13 Nov 2017 14:39:03 +0100 wenzelm tuned signature;
Thu, 27 Apr 2017 15:56:55 +0200 wenzelm clarified treatment of default port;
Tue, 18 Oct 2016 16:03:30 +0200 wenzelm clarified modules;
Sun, 16 Oct 2016 17:50:40 +0200 wenzelm tuned signature;
Sun, 16 Oct 2016 17:44:37 +0200 wenzelm simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
Sat, 15 Oct 2016 21:37:19 +0200 wenzelm clarified signature: more static types;
Thu, 13 Oct 2016 11:43:40 +0200 wenzelm tuned;
Wed, 12 Oct 2016 10:22:34 +0200 wenzelm explicit indication of Admin tools;
less more (0) tip