# HG changeset patch
# User wenzelm
# Date 1607860678 -3600
# Node ID d15c0c7ae0922d34c03189414c8f7be2da37167b
# Parent  6751057a64b1d459780a6cf4549f5dbd5bcfd5a3
full PIDE reports in batch build: see how it impacts overall performance;

diff -r 6751057a64b1 -r d15c0c7ae092 etc/options
--- a/etc/options	Sat Dec 12 20:02:46 2020 +0100
+++ b/etc/options	Sun Dec 13 12:57:58 2020 +0100
@@ -150,7 +150,7 @@
 option pide_reports : bool = true
   -- "report PIDE markup"
 
-option build_pide_reports : bool = false
+option build_pide_reports : bool = true
   -- "report PIDE markup in batch build"