# HG changeset patch
# User wenzelm
# Date 1678963447 -3600
# Node ID 08fcde7c55c07ac91a2ef35377625dfd5e8b8df3
# Parent  b9e9b818d7b0733508667c6cdb4e152dff7885a8
clarified ML option vs. Scala option (see also caa182bdab7a);

diff -r b9e9b818d7b0 -r 08fcde7c55c0 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed Mar 15 15:28:44 2023 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Thu Mar 16 11:44:07 2023 +0100
@@ -118,7 +118,7 @@
       |> Output.report;
     val _ =
       if not (null persistent_reports) andalso redirect andalso
-        not (Options.default_bool "build_pide_reports") andalso Future.enabled ()
+        not (Options.default_bool "pide_reports") andalso Future.enabled ()
       then
         Execution.print
           {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}