full PIDE reports in batch build: see how it impacts overall performance;
authorwenzelm
Sun, 13 Dec 2020 12:57:58 +0100
changeset 72892 d15c0c7ae092
parent 72891 6751057a64b1
child 72893 fbdadf5760c2
full PIDE reports in batch build: see how it impacts overall performance;
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"