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) } } }