diff -r 1b7c5d4b97a8 -r 47eb96592aa2 etc/options
--- 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"