author | wenzelm |
Sat, 19 Dec 2020 00:23:21 +0100 | |
changeset 72951 | 74339f1a5dd7 |
parent 72950 | ac6457a70db5 |
child 72952 | 09479be1fe2a |
--- a/src/Pure/System/isabelle_system.ML Sat Dec 19 00:08:14 2020 +0100 +++ b/src/Pure/System/isabelle_system.ML Sat Dec 19 00:23:21 2020 +0100 @@ -30,7 +30,7 @@ fun bash_output_check s = (case Bash.process s of - {rc = 0, out, ...} => (trim_line out) + {rc = 0, out, ...} => trim_line out | {err, ...} => error (trim_line err)); fun bash_output s =