aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/flags.mli
diff options
context:
space:
mode:
Diffstat (limited to 'lib/flags.mli')
-rw-r--r--lib/flags.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/flags.mli b/lib/flags.mli
index 0b00ac13c..7ce808041 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -49,6 +49,9 @@ val debug : bool ref
val in_debugger : bool ref
val in_toplevel : bool ref
+(** Enable STM debugging *)
+val stm_debug : bool ref
+
val profile : bool
(* Legacy flags *)