diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 374b5d597..74c5a02d5 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -22,7 +22,6 @@ open Pfedit open Constrextern open Ppconstr - let emacs_str s = if !Flags.print_emacs then s else "" let delayed_emacs_cmd s = |