etc/options
changeset 82729 d8986d88295e
parent 82677 c603d41dc183
--- a/etc/options	Mon Jun 16 12:18:26 2025 +0200
+++ b/etc/options	Mon Jun 16 12:19:23 2025 +0200
@@ -180,6 +180,9 @@
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
+public option ML_platform : string = "" for build build_sync
+  -- "explicit ML platform identifier"
+
 public option ML_system_64 : bool = false for build build_sync
   -- "prefer native 64bit platform (change requires restart)"