diff options
Diffstat (limited to 'lib/options.mli')
| -rw-r--r-- | lib/options.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/options.mli b/lib/options.mli index f990647473..59617ec34a 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -23,6 +23,8 @@ val term_quality : bool ref val xml_export : bool ref +val v7 : bool ref + val make_silent : bool -> unit val is_silent : unit -> bool val is_verbose : unit -> bool |