tree 35fb3757c6d0f9675b67f17b3472824fa511d6a7
parent a5efdb60905049e1224a020b78dd9699bdd15b29
author Paul Jakma <paul.jakma@hpe.com> 1455545466 +0000
committer Paul Jakma <paul.jakma@hpe.com> 1457459603 +0000

doc: Distribute a modern version of texinfo.tex with the docs

* doc/texinfo.tex: Ship a more recent texinfo.tex, from texinfo 6.1, so we
  don't have to worry about that.  E.g., this should allow UTF-8 unicode
  chars to be used directly in the text.
* doc/Makefile.am: Add previous to EXTRA_DIST