aboutsummaryrefslogtreecommitdiff
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 da43c86782..94c8795d45 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -47,6 +47,9 @@ val if_verbose : ('a -> unit) -> 'a -> unit
val make_auto_intros : bool -> unit
val is_auto_intros : unit -> bool
+val program_mode : bool ref
+val is_program_mode : unit -> bool
+
val make_warn : bool -> unit
val if_warn : ('a -> unit) -> 'a -> unit