[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: give --index-search example on man page
From: |
Karl Berry |
Subject: |
Re: give --index-search example on man page |
Date: |
Tue, 30 Sep 2014 17:44:41 GMT |
To do that, use "info -f grub -n
badram". (The current development version allows "info grub -n badram"
as well.) You can also do "info -n '(grub)'badram".
We should add two examples to the --help for this; finding an arbitrary
node without reference to menus or indices is useful.
> Also consider making an -i shortcut to reduce the pain.
IMHO that is not needed. (But if you want to do it, I certainly agree
that -I would be better than -i.)
Future versions will search in the indices for "badram" for the
command "info grub badram" if no "badram" entry is found in the
top-level menu of the "grub" file that it finds.
How about just searching for a node "badram" instead of involving the
indices? That seems more in line with what a user would expect.
Best,
Karl
- Re: give --index-search example on man page,
Karl Berry <=