etc/options
changeset 60730 02c2860fcf30
parent 60074 38a64cc17403
child 60765 e43e71a75838
--- a/etc/options	Thu Jul 16 11:10:57 2015 +0200
+++ b/etc/options	Thu Jul 16 11:38:18 2015 +0200
@@ -101,6 +101,9 @@
 public option ML_exception_trace : bool = false
   -- "ML exception trace for toplevel command execution"
 
+public option ML_debugger : bool = false
+  -- "ML debugger instrumentation for newly compiled code"
+
 public option ML_statistics : bool = true
   -- "ML runtime system statistics"