diff options
| author | Pierre Courtieu | 2017-05-04 11:25:22 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2017-05-04 11:25:22 +0200 |
| commit | 8bdb00bbea9dce95f7e0bc18250a41545660299d (patch) | |
| tree | b1fb490387750ee347f624b1a963dd2277d5726c /printing/printer.ml | |
| parent | 8bcf71360261d789ac3ab919bc49309df678628f (diff) | |
Warning removed.
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 1d3e67d9d6..91a7d22899 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -28,8 +28,6 @@ module CompactedDecl = Context.Compacted.Declaration let emacs_str s = if !Flags.print_emacs then s else "" -let delayed_emacs_cmd s = - if !Flags.print_emacs then s () else str "" let get_current_context () = Pfedit.get_current_context () |