# HG changeset patch
# User wenzelm
# Date 1607178475 -3600
# Node ID a44c30d08bb086b8e3781d72515016b888fca5a6
# Parent  eb526f6c92b7af5c4195b8278bea7710c2804da9
more robust batch-build;

diff -r eb526f6c92b7 -r a44c30d08bb0 src/Pure/ML/ml_compiler.ML
--- 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}