diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/options.ml | 1 | ||||
| -rw-r--r-- | lib/options.mli | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/lib/options.ml b/lib/options.ml index b2f2943aa..e59a19bbb 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -22,6 +22,7 @@ let batch_mode = ref false let debug = ref false let print_emacs = ref false +let print_emacs_safechar = ref false let term_quality = ref false diff --git a/lib/options.mli b/lib/options.mli index 9fa408d92..7fa55e636 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -17,6 +17,7 @@ val batch_mode : bool ref val debug : bool ref val print_emacs : bool ref +val print_emacs_safechar : bool ref val term_quality : bool ref |