From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jun 2005 09:45:59 +0000 (+0000)
Subject: clean now also performs clean_metas (since make also creates the metas)
X-Git-Tag: PRE_INDEX_1~43
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c0e1daa549d80d28caf54b8e0f1f019a5a83ac5;p=helm.git

clean now also performs clean_metas (since make also creates the metas)
---

diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in
index af199d3b5..b4b99eb24 100644
--- a/helm/ocaml/Makefile.in
+++ b/helm/ocaml/Makefile.in
@@ -37,7 +37,7 @@ metas: $(METAS)
 depend: $(MODULES:%=%.depend)
 install: $(MODULES:%=%.install)
 uninstall: $(MODULES:%=%.uninstall)
-clean: $(MODULES:%=%.clean)
+clean: clean_metas $(MODULES:%=%.clean)
 clean_metas:
 	rm -f $(METAS)
 distclean: clean clean_metas