Glenn Morris 29993416fb Add .info extension to @setfilename commands in doc/ ...

This makes no difference to anything, since we always use makeinfo -o,
but it makes automake happier, if we ever decide to use that.

2014-06-09 22:20:31 -04:00

13 KiB

Raw Blame History

View Raw