changeset 72728 | caa182bdab7a |
parent 72693 | 0201ae367518 |
child 72763 | 3cc73d00553c |
--- a/src/Pure/Tools/build.scala Thu Nov 26 17:01:19 2020 +0100 +++ b/src/Pure/Tools/build.scala Thu Nov 26 17:23:33 2020 +0100 @@ -202,7 +202,7 @@ options + "completion_limit=0" + "editor_tracing_messages=0" + - "pide_reports=false" // FIXME + ("pide_reports=" + options.bool("build_pide_reports")) val store = Sessions.store(build_options)