clarified ML option vs. Scala option (see also caa182bdab7a);

--- 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}