From 2e735eb94b7324c0e149fb4e884a7b405581eb4a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 26 Apr 2017 03:12:21 +0200 Subject: [stm] Tweak debug options. We allow for a dynamic setting of the STM debug flag, and we print some more information about the result of `process_transaction`. We also fix a printing bug due to mixing `Printf` and `Format`, which are not compatible. --- toplevel/usage.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'toplevel/usage.ml') diff --git a/toplevel/usage.ml b/toplevel/usage.ml index e29048035..feaf207b1 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -69,6 +69,7 @@ let print_usage_channel co command = \n -boot boot mode (implies -q and -batch)\ \n -bt print backtraces (requires configure debug flag)\ \n -debug debug mode (implies -bt)\ +\n -stm-debug STM debug mode (will trace every transaction) \ \n -emacs tells Coq it is executed under Emacs\ \n -noglob do not dump globalizations\ \n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ -- cgit v1.2.3