matitamake stuff:

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

diff --git a/helm/matita/matitaLog.ml b/helm/matita/matitaLog.ml
index 8c2e9a7a5826b0be8c5ec58d9661c39529368fd9..6ac82da58cd9b968b3eb0dcf5d7cc2dc0ac0a49f 100644 (file)
--- a/helm/matita/matitaLog.ml
+++ b/helm/matita/matitaLog.ml
@@ -53,6 +53,7 @@ let default_callback tag s =
 let callback = ref default_callback
 
 let set_log_callback f = callback := f
+let get_log_callback () = !callback
 
 let message s = !callback `Message s
 let warn s = !callback `Warning s