info: can we add a way to get the default path?

[Rob Browning <rlb@cs.utexas.edu>]

A long time back, I had needed to add /usr/local/XXX to my info path
to get some local info pages.  Unfortunately, since there info
provides no way to determine the default path, and since INFOPATH is
not normally set to anything, I had to set the full path in my
.bashrc:

  export INFOPATH=/usr/local/XXX:/usr/local/info:/usr/info

This worked OK, but I knew it was likely to be trouble.  Sure enough,
with the migration to /usr/share/info, things started breaking.

What I'm wondering is if it would make sense to augment info to
support either

  1) An option that tells it to print it's default path, say
     --print-default-path.  Then in your .bashrc, you could just say

        export INFOPATH=/usr/local/XXX:$(info --print-default-path)

  2) A magic token, that if put into the INFOPATH expands into the
     default path dynamically.  Something like this:

        export INFOPATH=/usr/local/XXX:@@DEFAULT_PATH@@

  3) A shell script config file like /etc/info.path that contained the
     right setting

        export DEFAULT_INFOPATH=/usr/local/info:/usr/share/info:/usr/info

Thoughts?  The last solution would require no source changes, but it
wouldn't be as dynamic as 2.  Method 2 would mean that you'd see
changes even if you don't log out between upgrades (not a big deal,
but slightly nicer...)

I'm happy to do the work if we decide we like one of these solutions.

Thanks

-- 
Rob Browning <rlb@cs.utexas.edu> PGP=E80E0D04F521A094 532B97F5D64E3930