diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-13 07:40:31 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-13 07:40:31 +0000 |
| commit | fc507c51aba9e0258e41e3ea4c8b38bf2cc0dc1b (patch) | |
| tree | 24c129848fc7a79255467bae9b1d16c1548f6f0f | |
| parent | a9662447f937057a9411ee5e6a6ba74fda93f989 (diff) | |
Make sure the initial state used in a protected loop is the state chose exactly
at the time the protected loop was started. This makes it possible
to have modifications of commands specific to the protected loop remembered
throughout the session.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1371 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/toplevel.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 35dde0bcf..ca5e27e11 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -292,7 +292,9 @@ let rec coq_switch b = protected_loop stdin with | Vernacinterp.Drop -> () - | Vernacinterp.ProtectedLoop -> coq_switch false + | Vernacinterp.ProtectedLoop -> + Lib.declare_initial_state(); + coq_switch false | End_of_input -> mSGERRNL [<>]; pp_flush(); exit 0 | Vernacinterp.Quit -> exit 0 | e -> |