Useless GrafiteTypes.get_baseuri removed.

[helm.git] / helm / software / components / grafite_engine / grafiteTypes.ml

diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index 9fd40b1c463af8c80b80002c4703b81cdbe1c8c8..959d96f368b4694ce69d9fe97db907eba6ab04f4 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -166,8 +166,6 @@ let add_moo_content cmds status =
     GrafiteAstPp.pp_command content')); *)
    status#set_moo_content_rev content'
 
-let get_baseuri status = status#baseuri;;
-
 let dump_status status = 
   HLog.message "status.aliases:\n";
   HLog.message "status.proof_status:";