changeset 72993 | 6ead333e450d |
parent 72992 | bcba32fd89de |
child 73012 | 238ddf525da4 |
--- 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)