From 21fe4c0eae8ec740e7d30dddc8cba4d287867d05 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 16 Mar 2006 09:50:06 +0000 Subject: [PATCH] fixed a bug in the Makefile, generatedGui.mli no more there --- helm/software/matita/Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index 7c54333cd..2dc38c3f1 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -153,6 +153,7 @@ cicbrowser.opt: matita.opt matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade $(H)$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml + $(H)rm -f matitaGeneratedGui.mli $(H)#$(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli .PHONY: clean -- 2.39.2