tuned comments;
authorwenzelm
Thu, 22 Sep 2022 10:38:52 +0200
changeset 76195 a1f458f089b9
parent 76194 d435f7b57212
child 76196 19978abbc111
tuned comments;
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"