Further improve make-dist checking
commit5531e75385ca3d02287f4df7788e38090f70b6b7
authorGlenn Morris <rgm@gnu.org>
Thu, 8 Dec 2016 00:45:48 +0000 (7 19:45 -0500)
committerGlenn Morris <rgm@gnu.org>
Thu, 8 Dec 2016 00:45:48 +0000 (7 19:45 -0500)
treecd91d6e990c85b3ab1103d9312db9ce6f794711c
parent953bf67fbea6298cb68b7610fdc09c3fcdf8aeec
Further improve make-dist checking

* make-dist: Print status messages when checking.
make-dist