Thanks, I installed the attached somewhat-different patch that should
fix the problems you mentioned.
From 8c038576a942c728f986c3d8a98b6edb63dd43ed Mon Sep 17 00:00:00 2001
From: Paul Eggert
Date: Sun, 3 Aug 2014 13:20:01 -0700
Subject: [PATCH] doc: prefer @env to @code
Reported by Benno Schulen
Hi,
In doc/grep.texi some environment variables are marked with
@code{} instead of @env{}. Attached patch fixes this.
There are some other env vars that still use @code{}, but
they refer to a "category" -- I don't quite know whether
these should be marked differently too, so I have left
them al