From 413007de240fefb28650bb5ba7940f46db656751 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 22 Mar 2008 11:21:10 +0000 Subject: [PATCH] since many stuff is under contrib, we need to ignore less directories --- helm/software/Makefile | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/helm/software/Makefile b/helm/software/Makefile index 99570786c..ce51f175b 100644 --- a/helm/software/Makefile +++ b/helm/software/Makefile @@ -54,12 +54,8 @@ NULL = DISTDIR = $(BASENAME)-$(MATITA_VERSION) CLEAN_ON_DIST = \ components/license \ - matita/TPTP/ \ - matita/dama/ \ - matita/dama_didactic/ \ - matita/library/freescale/ \ + matita/TPTP/ \ matita/contribs/ \ - matita/library_auto/ \ $(NULL) EXTRA_DIST = \ matita/AUTHORS \ -- 2.39.2