Subject: Re: texinfo files
To: None <>
From: Ted Lemon <>
List: current-users
Date: 09/22/1998 19:54:40
> They should be re-added and installed in /usr/share/info.

Actually, they should be built from source, not added.   The sources
are the .texi files.   In order for this to happen, though, the GNU
texinfo package needs to be installed on all build machines.