From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 25 Dec 2002 15:20:14 +0000 (+0000)
Subject: when making 'dist' remove old spurious dist directories
X-Git-Tag: v0_3_99~129
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d4993a3584bd83a87f642e8766eb86c0a24b682b;p=helm.git

when making 'dist' remove old spurious dist directories
---

diff --git a/helm/DEVEL/ocaml-http/Makefile b/helm/DEVEL/ocaml-http/Makefile
index a9495db9d..48c267589 100644
--- a/helm/DEVEL/ocaml-http/Makefile
+++ b/helm/DEVEL/ocaml-http/Makefile
@@ -76,6 +76,7 @@ distclean: clean docclean
 	-rm -f META
 dist: distreal distrm
 distreal: distclean depend
+	if [ -d $(DISTDIR) ]; then rm -rf $(DISTDIR); else true; fi
 	mkdir $(DISTDIR)
 	cp -r	\
 		$(patsubst %, %.ml, $(MODULES))	\