# HG changeset patch
# User wenzelm
# Date 1594675415 -7200
# Node ID 70bfda10f597946159dbc7071a13f42f0f432042
# Parent  a25c7c686176b1e9802930efdccf73cce97f7ca8
more robust;

diff -r a25c7c686176 -r 70bfda10f597 src/Pure/ML/ml_statistics.ML
--- a/src/Pure/ML/ml_statistics.ML	Mon Jul 13 23:10:47 2020 +0200
+++ b/src/Pure/ML/ml_statistics.ML	Mon Jul 13 23:23:35 2020 +0200
@@ -106,6 +106,6 @@
        TextIO.flushOut TextIO.stdOut;
        OS.Process.sleep (Time.fromReal delay);
        loop ());
-  in loop () end;
+  in loop () handle Interrupt => OS.Process.exit OS.Process.success end;
 
 end;