diff options
Diffstat (limited to 'lib/options.ml')
| -rw-r--r-- | lib/options.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/options.ml b/lib/options.ml index f2cc7a09de..90517561f1 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -25,10 +25,11 @@ let term_quality = ref false let xml_export = ref false let v7 = ref true +let v7_only = ref false (* Translate *) let translate = ref false -let make_translate f = translate := f; () +let make_translate f = translate := f; v7 := f; () let do_translate () = !translate let translate_file = ref false |