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 4558a011cb2b22fb99740be45c612492d3ef2683..2968a240512c20633d8a20816f3ba21ae23dca58 100644 (file)
--- 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