author | wenzelm |
Thu, 22 Sep 2022 10:38:52 +0200 | |
changeset 76195 | a1f458f089b9 |
parent 76194 | d435f7b57212 |
child 76196 | 19978abbc111 |
etc/options | file | annotate | diff | comparison | revisions |
--- 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"