diff options
Diffstat (limited to 'lib/flags.mli')
| -rw-r--r-- | lib/flags.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index 30d1b5b2bd..ebd23a4d20 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -41,6 +41,7 @@ val load_vos_libraries : bool ref (** Debug flags *) val debug : bool ref +val xml_debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref |