# HG changeset patch # User wenzelm # Date 1568548898 -7200 # Node ID e54213954efcd665e593214b01afe7781c24e7c4 # Parent 4b3cfd73f428b00a4e0dfeeb6ec75fb4da84c6f0 more ambitious options (again); diff -r 4b3cfd73f428 -r e54213954efc src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Sun Sep 15 13:52:30 2019 +0200 +++ b/src/Pure/Tools/dump.scala Sun Sep 15 14:01:38 2019 +0200 @@ -212,7 +212,7 @@ val use_theories_result = session.use_theories(used_theories.map(_.theory), unicode_symbols = unicode_symbols, - share_common_data = false /* FIXME true */, + share_common_data = true, progress = progress, checkpoints = deps.dump_checkpoints, commit = Some(Consumer.apply _))