# HG changeset patch # User wenzelm # Date 1608333801 -3600 # Node ID 74339f1a5dd792d1c69fdcf43d69ba67518d50f7 # Parent ac6457a70db5d52ca873d1cac635843fe166d724 tuned; diff -r ac6457a70db5 -r 74339f1a5dd7 src/Pure/System/isabelle_system.ML --- 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 =