aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printer.ml')
-rw-r--r--printing/printer.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index 1d3e67d9d..91a7d2289 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 ()