See https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=941557;msg=28
--- doc/gri.texi.orig	2019-12-23 09:28:19.000000000 -0700
+++ doc/gri.texi	2019-12-23 09:36:48.000000000 -0700
@@ -1,4 +1,5 @@
 \input texinfo 
+@documentencoding ISO-8859-1
 
 @c
 @comment *** Start of HTML stuff ***