diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/pp.ml4 | 1 | ||||
| -rw-r--r-- | lib/pp.mli | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 3244993377..d4e6eb722b 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -17,6 +17,7 @@ open Pp_control [Pp] -> [Options] *) let print_emacs = ref false let make_pp_emacs() = print_emacs:=true +let make_pp_nonemacs() = print_emacs:=false (* The different kinds of blocks are: \begin{description} diff --git a/lib/pp.mli b/lib/pp.mli index d4248cc7f2..7b9d7d6637 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -16,6 +16,7 @@ open Pp_control chars inserted at some places). This function should called once in module [Options], that's all. *) val make_pp_emacs:unit -> unit +val make_pp_nonemacs:unit -> unit (* Pretty-printers. *) |