copied text is unlocked :)

[helm.git] / helm / matita / matitaScript.mli

diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli
index cbdfb286bbdef58e8d0eb54448a7776a483afd1a..ab39b9cfd956c75b9b41147a36bbea5e3bac8ada 100644 (file)
--- a/helm/matita/matitaScript.mli
+++ b/helm/matita/matitaScript.mli
@@ -60,6 +60,9 @@ object
 
   (** end of script, true if the whole script has been executed *)
   method eos: bool
+
+  (** misc *)
+  method clean_dirty_lock: unit
   
   (* debug *)
   method dump : unit -> unit