Quieten make-dist default operation
commit75c9314cbf01e048f9626b26233b2de7b9cdba65
authorGlenn Morris <rgm@gnu.org>
Thu, 8 Dec 2016 00:59:14 +0000 (7 19:59 -0500)
committerGlenn Morris <rgm@gnu.org>
Thu, 8 Dec 2016 00:59:14 +0000 (7 19:59 -0500)
tree153d0811322317159fbc2dbeabc86e8d73bedb74
parent55c1937e52625c68d5f9de332bbd47f7def5d1c0
Quieten make-dist default operation

* make-dist: Add --verbose option.  Default to quieter operation.
make-dist