provide execute operation, similar to Isabelle_System.bash;
authorwenzelm
Mon, 10 Oct 2016 21:52:55 +0200
changeset 64135 865dda40e1cc
parent 64134 57581e4026fe
child 64136 7c5191489457
provide execute operation, similar to Isabelle_System.bash;
src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Oct 10 21:44:54 2016 +0200
+++ b/src/Pure/General/ssh.scala	Mon Oct 10 21:52:55 2016 +0200
@@ -255,6 +255,13 @@
 
     def close { session.disconnect }
 
+    def execute(command: String,
+        options: Options = session_options,
+        progress_stdout: String => Unit = (_: String) => (),
+        progress_stderr: String => Unit = (_: String) => (),
+        strict: Boolean = true): Process_Result =
+      exec(command, options).result(progress_stdout, progress_stderr, strict)
+
     def exec(command: String, options: Options = session_options): Exec =
     {
       val kind = "exec"