changeset 77330 | 47eb96592aa2 |
parent 77149 | 3991a35cd740 |
child 77363 | cbd053fff24c |
--- a/etc/options Tue Feb 21 11:20:42 2023 +0100 +++ b/etc/options Tue Feb 21 12:03:52 2023 +0100 @@ -172,7 +172,7 @@ -- "ML process command prefix (process policy)" -section "PIDE Build" +section "Build Process" option pide_reports : bool = true -- "report PIDE markup (in ML)" @@ -180,6 +180,9 @@ option build_pide_reports : bool = true -- "report PIDE markup (in batch build)" +option build_engine : string = "" + -- "alternative session build engine" + section "Editor Session"