1) grafiteWalker removed

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

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 658a3ad384bb5d94ee2826b3239c530b94ad2b6f..cc46c76492e43218f24ed1779beb4b720711f78f 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -140,7 +140,7 @@ let _ =
       ignore (GMenu.separator_item ~packing:gui#main#debugMenu_menu#append ())
     in
     addDebugItem "dump aliases" (fun _ ->
-      let status = GrafiteTypes.get_lexicon script#grafite_status in
+      let status = GrafiteTypes.get_estatus script#grafite_status in
       LexiconEngine.dump_aliases HLog.debug "" status);
 (* FG: DEBUGGING   
     addDebugItem "dump interpretations" (fun _ ->