Bug solved: X-style paste (i.e. paste of the PRIMARY selection using the

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

diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli
index 258a72e0c13fc3cc748e578073a0ef12dcfcb92e..2cc559a3b0a790e751c8f9e466b90129eb3a329f 100644 (file)
--- a/helm/matita/matitaScript.mli
+++ b/helm/matita/matitaScript.mli
@@ -27,6 +27,7 @@ class type script =
 object
 
   method locked_mark : Gtk.text_mark
+  method locked_tag : GText.tag
 
   (** @return current status *)
   method status: MatitaTypes.status