# HG changeset patch
# User wenzelm
# Date 1614009536 -3600
# Node ID a96944cbaf7d4247651245da7167d2b7e45088b6
# Parent  37aff2142295746ac7febdea2bf6c65d953e57d2
tuned;

diff -r 37aff2142295 -r a96944cbaf7d src/Pure/System/process_result.ML
--- a/src/Pure/System/process_result.ML	Mon Feb 22 16:54:33 2021 +0100
+++ b/src/Pure/System/process_result.ML	Mon Feb 22 16:58:56 2021 +0100
@@ -41,6 +41,8 @@
 val err_lines = #err_lines o rep;
 val timing = #timing o rep;
 
+end;
+
 val out = trim_line o cat_lines o out_lines;
 val err = trim_line o cat_lines o err_lines;
 
@@ -49,5 +51,3 @@
 fun check result = if ok result then result else error (err result);
 
 end;
-
-end;