src/Pure/Tools/build.scala
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)