snapshot, notably:

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

diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli
index afaa631a08f01646e773aa505301c710db2718d3..36318dc1fa0d2dbafa956c15e9336a92a902da3f 100644 (file)
--- a/helm/matita/matitaMisc.mli
+++ b/helm/matita/matitaMisc.mli
@@ -66,3 +66,6 @@ class shell_history : int -> [string] history
   * @param first element in history (this history is never empty) *)
 class ['a] browser_history: ?memento:'a memento -> int -> 'a -> ['a] history
 
+  (** {2 db handling} *)
+val dbd_instance: unit -> Mysql.dbd
+