+ chmod -R u+w $(distdir)/doc
...
- echo "Distribution date: `date`" >> README
+ echo "Distribution date: `date`" >> $(distdir)/READMEOk, pushed. Thanks.
+ chmod -R u+w $(distdir)/doc
...
- echo "Distribution date: `date`" >> README
+ echo "Distribution date: `date`" >> $(distdir)/READMEOk, pushed. Thanks.