--- distdir.am Sun Jul 21 21:31:06 2002
+++ distdir.am.new Mon Aug 19 20:14:41 2002
@@ -98,10 +98,11 @@
## source files _and_ generated files. It is also important when the
## directory exists only in $(srcdir), because some vendor Make (such
## as Tru64) will magically create an empty directory in `.'
+## DO NOT FORGET that there may be duplicates in the source and build :-(
if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \
cp -pR $(srcdir)/$$file $(distdir)$$dir || exit 1; \
fi; \
- cp -pR $$d/$$file $(distdir)$$dir || exit 1; \
+ cp -pR $$d/$$file $(distdir)$$dir || :; \
else \
## Test for file existence because sometimes a file gets included in
## DISTFILES twice. For example this happens when a single source
