diff options
| -rw-r--r-- | toplevel/toplevel.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index bc50eb43de..ee28156a37 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -343,8 +343,11 @@ let feed_emacs = function let rec loop () = Sys.catch_break true; if !Flags.print_emacs then begin + (* TODO : check with Enrico ?! *) + (* Pp.set_feeder feed_emacs; Vernacentries.enable_goal_printing := false; + *) Vernacentries.qed_display_script := false; end; try |