* admin/admin.el (make-manuals): Don't bother with txt or dvi any more.
commit0cb70db774efa7a7b30f26771276039e089ce528
authorGlenn Morris <rgm@gnu.org>
Sat, 29 Jun 2013 01:51:32 +0000 (28 18:51 -0700)
committerGlenn Morris <rgm@gnu.org>
Sat, 29 Jun 2013 01:51:32 +0000 (28 18:51 -0700)
tree1759fb56958804dd6b859214af34db70619ec33d
parentdf03dc8a4cf51560caeae66e98062e70fb5cbfbc
* admin/admin.el (make-manuals): Don't bother with txt or dvi any more.
(manual-txt): Remove.
(manual-pdf): Doc fix.
(manual-ps): Rename from manual-dvi.
admin/ChangeLog
admin/admin.el