# HG changeset patch # User wenzelm # Date 1608761949 -3600 # Node ID 6ead333e450d7dcbc05e26c4179d6933b5549c09 # Parent bcba32fd89dedfbc058c3984383b3c0c26df22d0 more robust defaults: spurious problems with parallel invocations and interrupts; diff -r bcba32fd89de -r 6ead333e450d src/HOL/ROOT --- a/src/HOL/ROOT Wed Dec 23 23:08:57 2020 +0100 +++ b/src/HOL/ROOT Wed Dec 23 23:19:09 2020 +0100 @@ -377,6 +377,7 @@ Author: Jasmin Blanchette, TU Muenchen Copyright 2009 " + options [kodkod_scala] sessions "HOL-Library" theories [quick_and_dirty] Nitpick_Examples diff -r bcba32fd89de -r 6ead333e450d src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Dec 23 23:08:57 2020 +0100 +++ b/src/Pure/Tools/build.scala Wed Dec 23 23:19:09 2020 +0100 @@ -202,6 +202,7 @@ options + "completion_limit=0" + "editor_tracing_messages=0" + + "kodkod_scala=false" + ("pide_reports=" + options.bool("build_pide_reports")) val store = Sessions.store(build_options)