# 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 =