# HG changeset patch
# User wenzelm
# Date 1594825826 -7200
# Node ID bc85d93aad23c2d6cb43a721a143afed630f5a85
# Parent  c6756adfef0f80b7572d59a76899ff1d449ab1e0
more robust: handle unavailable statistics;

diff -r c6756adfef0f -r bc85d93aad23 src/Pure/ML/ml_statistics.ML
--- a/src/Pure/ML/ml_statistics.ML	Wed Jul 15 16:28:26 2020 +0200
+++ b/src/Pure/ML/ml_statistics.ML	Wed Jul 15 17:10:26 2020 +0200
@@ -133,6 +133,7 @@
        TextIO.flushOut TextIO.stdOut;
        OS.Process.sleep (Time.fromReal delay);
        loop ());
-  in loop () handle Interrupt => OS.Process.exit OS.Process.success end;
+    fun exit () = OS.Process.exit OS.Process.success;
+  in loop () handle Interrupt => exit () | Fail _ => exit () end;
 
 end;