# HG changeset patch
# User wenzelm
# Date 1596806030 -7200
# Node ID b9ded33bd58ce869f8cfd76b9ec324fb0a81ebdd
# Parent  16fab31feadc8c06e69a99077e960773810f6527
clarified catch-all handler --- avoid confusion of Interrupt vs. Exn.Interrupt in varying ML contexts;

diff -r 16fab31feadc -r b9ded33bd58c src/Pure/ML/ml_statistics.ML
--- a/src/Pure/ML/ml_statistics.ML	Fri Aug 07 11:46:14 2020 +0200
+++ b/src/Pure/ML/ml_statistics.ML	Fri Aug 07 15:13:50 2020 +0200
@@ -140,6 +140,6 @@
        OS.Process.sleep (Time.fromReal delay);
        loop ());
     fun exit () = OS.Process.exit OS.Process.success;
-  in loop () handle Interrupt => exit () | Fail _ => exit () end;
+  in loop () handle _ (*sic!*) => exit () end;
 
 end;