Todd Vierling writes:
> On Tue, 22 Sep 1998, Michael C. Richardson wrote:
> 
> :   Yes, I agree. My later points were that the files are rather dependant
> : on the GNU makefiles, and on things outside that directory, so getting 
> : everything to build nicely make be more complicated than just invoking
> : "makeinfo" at the right place.
> 
> At the current time, stuff being imported into gnu/dist _does_ have
> pre-generated `.info' files, though those are currently "deleted" at the
> head of the CVS tree.  It would be trivial to re-add these files.

They should be re-added and installed in /usr/share/info.

Perry