# HG changeset patch
# User wenzelm
# Date 1442428686 -7200
# Node ID 9d0834562a78730e7232e5bacc5c0a67a4155d81
# Parent  b6b5e41d261b39384272c1c4d5b2fa7efd7ee4fc
tuned whitespace;

diff -r b6b5e41d261b -r 9d0834562a78 src/Pure/Concurrent/time_limit.ML
--- a/src/Pure/Concurrent/time_limit.ML	Wed Sep 16 16:34:33 2015 +0200
+++ b/src/Pure/Concurrent/time_limit.ML	Wed Sep 16 20:38:06 2015 +0200
@@ -36,4 +36,3 @@
     end);
 
 end;
-