From 5578fb7245540a757e319a8343d1cbbff9276490 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 8 Sep 2014 13:47:27 +0200
Subject: BackTo not part of the doc when used by emacs

Used to work "by chance".
---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 407c1ed1c7..5c9e1cf605 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 ->
-- 
cgit v1.2.3