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

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 811b1a858a4b98f873445d76ee4d247d08f8f834..af7b02a82f70a9e6765562b44413ca125418a13d 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -467,6 +467,7 @@ object (self)
   val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"]
 
   method locked_mark = locked_mark
+  method locked_tag = locked_tag
 
     (* history can't be empty, the invariant above grant that it contains at
      * least the init status *)