diff options
Diffstat (limited to 'lib/pp.ml4')
| -rw-r--r-- | lib/pp.ml4 | 1 |
1 files changed, 1 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} |