--- a/src/Pure/ML/ml_compiler.ML Sat Dec 05 14:36:41 2020 +0100
+++ b/src/Pure/ML/ml_compiler.ML Sat Dec 05 15:27:55 2020 +0100
@@ -117,7 +117,8 @@
|> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
|> Output.report;
val _ =
- if not (null persistent_reports) andalso redirect andalso Future.enabled ()
+ if not (null persistent_reports) andalso redirect andalso
+ not (Options.default_bool "build_pide_reports") andalso Future.enabled ()
then
Execution.print
{name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}