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
--
To UNSUBSCRIBE, email to [EMAIL PROTECTED]
with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]
