Thanks, Josip, for your answer. To conclude -- am I right with
the following statements?
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.
2. The directory index should be a file called /usr/info/dir;
it is an error if this file is gzipped.
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.
Thanks,
Marco
--
Marco Kuhlmann [EMAIL PROTECTED]
--
To UNSUBSCRIBE, email to [EMAIL PROTECTED]
with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]
