diff options
| author | gareuselesinge | 2013-08-30 14:07:45 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-08-30 14:07:45 +0000 |
| commit | e5107d729c377eeb38602e6e2af1ffd9bd577966 (patch) | |
| tree | d9b09db50e14ee992a2f1da4c3f61abce8bdb2ae | |
| parent | edcbdc62851c4ebef50ac8b2f67869f557e80242 (diff) | |
When PG is used as interface behave as before STM
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16748 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/toplevel.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index da3049141b..bc50eb43de 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -308,7 +308,7 @@ let do_vernac () = resynch_buffer top_buffer; try Vernac.eval_expr (read_sentence ()); - if not !Flags.print_emacs then Stm.finish () + Stm.finish () with | End_of_input | Errors.Quit -> msgerrnl (mt ()); pp_flush(); raise Errors.Quit |