From 8708cd63ee4604665d2f9eff0153931bd17c25bb Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Jul 2014 16:00:07 +0200
Subject: STM: export the observe function (useful for pide)

---
 stm/stm.mli | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/stm/stm.mli b/stm/stm.mli
index fd306425c1..e5327cb838 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -38,6 +38,8 @@ val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
 (* Evaluates the tip of the current branch *)
 val finish : unit -> unit
 
+val observe : Stateid.t -> unit
+
 val stop_worker : int -> unit
 
 (* Joins the entire document.  Implies finish, but also checks proofs *)
-- 
cgit v1.2.3