diff -r 13f4056c42d7 -r ea6a4c8bc722 etc/options
--- a/etc/options	Fri Sep 11 17:48:49 2015 +0200
+++ b/etc/options	Fri Sep 11 17:57:34 2015 +0200
@@ -107,6 +107,9 @@
 public option ML_statistics : bool = true
   -- "ML run-time system statistics"
 
+public option ML_system_64 : bool = false
+  -- "ML system for 64bit platform is used if possible (change requires restart)"
+
 
 section "Editor Reactivity"