when making 'dist' remove old spurious dist directories

diff --git a/helm/DEVEL/ocaml-http/Makefile b/helm/DEVEL/ocaml-http/Makefile
index a9495db9d17e6536224de5d1a967492861b45ff2..48c26758986b9c45d958f8a44cec1992951af745 100644 (file)
--- 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)) \