snapshot, notably:

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index f8f252b524f3e3e697b6ae12f339bde0cbb1bd54..de5240e447ccacbf533609fe91f6b59f44e49f09 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -123,6 +123,7 @@ class gui file =
 *)
 
     method about = about
+    method browser = browser
     method check = check
     method console = console
     method fileSel = fileSel