src/Pure/System/bash.scala
changeset 73134 8a8ffe78eee7
parent 72598 d9f2be66ebad
child 73228 0575cfd2ecfc
--- a/src/Pure/System/bash.scala	Sat Jan 16 15:43:54 2021 +0100
+++ b/src/Pure/System/bash.scala	Sat Jan 16 17:02:14 2021 +0100
@@ -199,7 +199,7 @@
 
       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
 
-      Process_Result(rc, out_lines.join, err_lines.join, false, get_timing)
+      Process_Result(rc, out_lines.join, err_lines.join, get_timing)
     }
   }
 }