# HG changeset patch
# User wenzelm
# Date 1476129175 -7200
# Node ID 865dda40e1cc534d97f39b346a04d5e0700a402b
# Parent  57581e4026feefa5e7203705676d8bcbc576cff5
provide execute operation, similar to Isabelle_System.bash;

diff -r 57581e4026fe -r 865dda40e1cc 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"