# HG changeset patch
# User wenzelm
# Date 1230392030 -3600
# Node ID d41ccf3efbfc91c9e05c3989080490b01b3fd42e
# Parent  0e88d33e8d19a7820a782c404c0cad8dd5036324
refined execute, which replaces exec/exec2;

diff -r 0e88d33e8d19 -r d41ccf3efbfc src/Pure/Tools/isabelle_process.scala
--- a/src/Pure/Tools/isabelle_process.scala	Sat Dec 27 16:33:19 2008 +0100
+++ b/src/Pure/Tools/isabelle_process.scala	Sat Dec 27 16:33:50 2008 +0100
@@ -125,7 +125,7 @@
     if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
     else {
       try {
-        if (isabelle_system.exec("kill", "-INT", pid).waitFor == 0)
+        if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
           put_result(Kind.SIGNAL, null, "INT")
         else
           put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
@@ -360,7 +360,7 @@
     try {
       val cmdline =
         List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
-      proc = isabelle_system.exec2(cmdline: _*)
+      proc = isabelle_system.execute(true, cmdline: _*)
     }
     catch {
       case e: IOException =>