--- a/etc/options Thu Nov 26 17:01:19 2020 +0100
+++ b/etc/options Thu Nov 26 17:23:33 2020 +0100
@@ -150,6 +150,9 @@
option pide_reports : bool = true
-- "report PIDE markup"
+option build_pide_reports : bool = false
+ -- "report PIDE markup in batch build"
+
section "Editor Session"