tuned comment;
authorwenzelm
Wed, 12 Oct 2022 13:01:06 +0200
changeset 76276 13b733e78c26
parent 76275 b446004b2464
child 76277 f0d8f659b19a
tuned comment;
etc/options
--- a/etc/options	Wed Oct 12 11:15:36 2022 +0200
+++ b/etc/options	Wed Oct 12 13:01:06 2022 +0200
@@ -161,7 +161,7 @@
   -- "ML debugger instrumentation for newly compiled code"
 
 public option ML_system_64 : bool = false
-  -- "ML system for 64bit platform is used if possible (change requires restart)"
+  -- "prefer native 64bit platform (change requires restart)"
 
 public option ML_system_apple : bool = true
   -- "prefer native Apple/ARM64 platform (change requires restart)"