# HG changeset patch
# User wenzelm
# Date 1568548350 -7200
# Node ID 4b3cfd73f428b00a4e0dfeeb6ec75fb4da84c6f0
# Parent  3eb30d80cee62790a907ee30493b432d8c4f43f3
more ambitious options (again, after 93aa546ffbac);

diff -r 3eb30d80cee6 -r 4b3cfd73f428 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sun Sep 15 13:42:01 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Sun Sep 15 13:52:30 2019 +0200
@@ -214,7 +214,7 @@
             unicode_symbols = unicode_symbols,
             share_common_data = false /* FIXME true */,
             progress = progress,
-            checkpoints = Set.empty /* FIXME deps.dump_checkpoints */,
+            checkpoints = deps.dump_checkpoints,
             commit = Some(Consumer.apply _))
 
         val bad_theories = Consumer.shutdown()