diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 94c6ed1f5..d64fb38e5 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -335,7 +335,8 @@ let init is_ide = end; if !batch_mode then (flush_all(); - if !output_context then Pp.ppnl (Prettyp.print_full_pure_context ()); + if !output_context then + Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ()); Profile.print_profile (); exit 0); Lib.declare_initial_state () |