| commit | 953bf67fbea6298cb68b7610fdc09c3fcdf8aeec | |
| author | Glenn Morris <rgm@gnu.org> | |
| Thu, 8 Dec 2016 00:43:36 +0000 (7 19:43 -0500) | ||
| committer | Glenn Morris <rgm@gnu.org> | |
| Thu, 8 Dec 2016 00:43:36 +0000 (7 19:43 -0500) | ||
| tree | 20efbc67ff34e46b642a44f1ffdd68f0d6e6cfc0 | treesnapshot (tar.gz zip) |
| parent | 129645a7a7129f2a63c1daf2743c2d901460b9fa | commitdiff |
Improve previous make-dist change
* make-dist: Let make check the info files more thoroughly.
* make-dist: Let make check the info files more thoroughly.
| make-dist | diffblobblamehistory |