gri-texinfo-6.7patch.txt 357 B

1234567891011
  1. diff -Naur gri-2.12.23/doc/gri.texi gri-2.12.23-new/doc/gri.texi
  2. --- gri-2.12.23/doc/gri.texi 2017-08-24 15:31:52.000000000 +0100
  3. +++ gri-2.12.23-new/doc/gri.texi 2019-10-22 16:13:33.476840964 +0100
  4. @@ -1,5 +1,5 @@
  5. \input texinfo
  6. -
  7. +@documentencoding ISO-8859-1
  8. @c
  9. @comment *** Start of HTML stuff ***
  10. @comment # HTML support, via comments in texinfo: