# HG changeset patch
# User wenzelm
# Date 1663835932 -7200
# Node ID a1f458f089b9421d882c8ccf56fe77bee32d0ab7
# Parent  d435f7b57212adc47337a9baac14065f409222c5
tuned comments;

diff -r d435f7b57212 -r a1f458f089b9 etc/options
--- a/etc/options	Tue Sep 20 20:12:01 2022 +0000
+++ b/etc/options	Thu Sep 22 10:38:52 2022 +0200
@@ -170,10 +170,10 @@
 section "PIDE Build"
 
 option pide_reports : bool = true
-  -- "report PIDE markup"
+  -- "report PIDE markup (in ML)"
 
 option build_pide_reports : bool = true
-  -- "report PIDE markup in batch build"
+  -- "report PIDE markup (in batch build)"
 
 
 section "Editor Session"