diff options
Diffstat (limited to 'academic/gri/gri-texinfo-6.7patch.txt')
| -rw-r--r-- | academic/gri/gri-texinfo-6.7patch.txt | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/academic/gri/gri-texinfo-6.7patch.txt b/academic/gri/gri-texinfo-6.7patch.txt new file mode 100644 index 0000000000000..f9b2dedf914f3 --- /dev/null +++ b/academic/gri/gri-texinfo-6.7patch.txt @@ -0,0 +1,10 @@ +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: |