path: root/academic/gri/gri-texinfo-6.7patch.txt

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