From: Stefano Zacchiroli Date: Fri, 3 Feb 2006 15:19:37 +0000 (+0000) Subject: do not delete Makefile and Makefile.common on distclean since they are no X-Git-Tag: make_still_working~7649 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cf59c0f6b6e082b49caaf7ba3745e08b1a845be5;p=helm.git do not delete Makefile and Makefile.common on distclean since they are no longer generated at configure time --- diff --git a/helm/ocaml/Makefile b/helm/ocaml/Makefile index 4558a011c..2968a2405 100644 --- a/helm/ocaml/Makefile +++ b/helm/ocaml/Makefile @@ -62,7 +62,7 @@ EXTRA_DIST_CLEAN = \ distclean: clean clean_metas rm -f $(METAS) rm -f configure config.log config.cache config.status - rm -f Makefile Makefile.common $(EXTRA_DIST_CLEAN) + rm -f $(EXTRA_DIST_CLEAN) .PHONY: all opt world metas depend install uninstall clean clean_metas distclean