diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-08 13:47:27 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-09 13:11:38 +0200 |
| commit | 5578fb7245540a757e319a8343d1cbbff9276490 (patch) | |
| tree | f58eaa0e4562ce88401ecc8496656605e2fa1c65 | |
| parent | b280ff870833a775564900d30d00a43d63246f8a (diff) | |
BackTo not part of the doc when used by emacs
Used to work "by chance".
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 407c1ed1c..5c9e1cf60 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1492,7 +1492,7 @@ end = struct VtStm (VtBack oid, true), VtLater | VernacBacktrack (id,_,_) | VernacBackTo id -> - VtStm (VtBack (Stateid.of_int id), true), VtNow + VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow | _ -> VtUnknown, VtNow with | Not_found -> |