On Thu, Oct 26, 2000 at 09:08:00AM +0200, Marco Kuhlmann wrote: > 1. Although the Debian Policy says that info documents should > be put into /usr/share/info, they really *shall* be put into > /usr/info for compatibility reasons.
No, actually, it's just the dir file that stays in /usr/info. The info documents should be installed in /usr/share/info directory. > 2. The directory index should be a file called /usr/info/dir; > it is an error if this file is gzipped. Correct. > 3. /usr/share/info should not contain a dir file, be it gzipped > or not. Instead, the info documents in /usr/share/info should > be indexed by /usr/info/dir. Correct. -- Digital Electronic Being Intended for Assassination and Nullification
