history man page

[Julien ÉLIE]

Hi,

Shouldn't we change the name of the history man page?
Because it is quite hard to view!

I always obtain "history - GNU History Library" and I think
it is the same for other people.
Even with the Debian package, it does not work (I have checked,
in case my installation from sources had not been done well).


% man -w history
/usr/share/man/man3/history.3readline.gz


Note that I have the right $MANPATH set:

% man -w active
/home/news/share/man/man5/active.5

% ls /home/news/share/man/man5/history.5
/home/news/share/man/man5/history.5


I also have:

% man -f history
history (3readline)  - GNU History Library
history (5)          - record of current and recently expired Usenet articles

It is listed here, but I cannot access it...

-- 
Julien ÉLIE

« Le travail n'est pas une bonne chose. Si ça l'était,
  les riches l'auraient accaparé. »