etc/options

--- a/etc/options	Sun Feb 26 20:52:14 2023 +0100
+++ b/etc/options	Sun Feb 26 21:05:39 2023 +0100
@@ -177,6 +177,9 @@
 option build_pide_reports : bool = true
   -- "report PIDE markup (in batch build)"
 
+option build_hostname : string = ""
+  -- "alternative hostname for build process (default $ISABELLE_HOSTNAME)"
+
 option build_engine : string = ""
   -- "alternative session build engine"