patchAdd --info-path and --man-path options to git.

To better support git extensions provided by 3rd parties which would like to install their own man pages and Info files in the same place as git's own man pages and Info files add support for --man-path and --info-path options.

Signed-off-by: Jon Seymour <jon.seymour@gmail.com>
---
 Documentation/git.txt |   10 +++++++++-
 Makefile              |    4 +++-
 git.c                 |    8 +++++++-
 3 files changed, 19 insertions(+), 3 deletions(-)

Jon Seymour <jon.seymour@gmail.com> writes:

This an improvement that is pretty much independent from the issue of third party extensions. In fact, even people who would oppose to the idea of any third party crap [*1*] contaminating the install directories owned by git may want to this patch.

It is useful to have these options even for read-only users. Cf. 89a56bf (add --html-path to get the location of installed HTML docs, 2009-04-05).

I'll rewrite the proposed commit message before queuing this to 'pu'.

Thanks.

[Footnote]

*1* Not all extensions may be crappy, but some extension will be, and you may find out the crappiness only after installing it, but at that point it already has contaminated your git directories.

On Mon, May 2, 2011 at 4:15 AM, Junio C Hamano <gitster@pobox.com> wrote:

Thanks.

I agree the sentiment that suggests that we don't want to pollute git's own directories with 3rd party contributions.

This, indeed, is part of the motivation for a --plugins-path option which would provide a physically separate location for 3rd party contributions, per the earlier discussions between yourself and Jonathan Nieder. I'll put together a suggested patch for how this might work in the next week or so.

jon.

Junio C Hamano wrote:

I don't mind this patch at all, but I do not have a full picture yet of how it helps.

In the case of HTML, the standard way to show git documentation in your custom documentation viewer is to pull up file://$(git --html-path)/index.html, using the full path to the HTML files. So if "git gui" were to gain a documentation viewer widget instead of relying on git web--browse, it would need the HTML path.

By contrast, man and info typically use standard search mechanisms: man using $MANPATH and info using the dir.info file. The usual interface to git's documentation through a man browser is not

	man /usr/share/man/man1/git-add.1.gz

but

	man git-add;	# or "man git add" if your man viewer supports it

And the usual interface through an info browser is

	info git

.

So it is not clear to me how this would help when you want to view documentation. Similarly, if you want to sneak documentation into an existing git installation (ignoring the question of whether that's a good idea), using HTML you would have to modify git's index.html and add your HTML files alongside it, while using "man" or "info" you would have to modify the index page (git.1 or gitman.info) but could put your custom pages wherever you want in the viewer's search path.

So while I can't see the harm in exposing --info-path and --man-path, the current patch seems to do an incomplete job of documenting them. Perhaps this is about finding the documentation corresponding to a particular copy of git when a machine has multiple copies?

Hi again,

Two quick corrections.

Jonathan Nieder wrote:

Actually, it already uses the HTML path. :)

It seems Jon's and my mails crossed. Here's another use case for --man-path: if your frontend wants to fall back to HTML documentation without spawning a man pager when the manpages are not installed, it needs to know where to look.

(See also gitgui-0.6.0~32, git-gui: Offer quick access to the HTML formatted documentation, 2007-01-28)

Jonathan Nieder <jrnieder@gmail.com> writes:

I think you are forgetting the case where the git-man-path the user uses to install git may be outside /usr/share/man (e.g. $HOME/share/man). In such an installation, by setting $PATH to include your installed git binary (e.g. $HOME/bin), you should be able to say "git help -m git" to tell help.c to internally prepend $HOME/share/man to the $MANPATH before it kicks "man". Does "man git-add" work without you knowing where that directory is (iow, without having $HOME/share/man on $MANPATH)? And if it does not, how would you learn what directory to add to your $MANPATH?

Isn't that what this patch is solving? I am not sure where the similarity with the html documentation breaks donw. The same thing for info.

On Mon, May 2, 2011 at 10:02 AM, Junio C Hamano <gitster@pobox.com> wrote:

Good point. For non-distro installed installations of git, this would be handy, even for read-only purposes.

jon.

On Mon, May 2, 2011 at 10:06 AM, Jon Seymour <jon.seymour@gmail.com> wrote:

BTW: should it be --man-path and --info-path or --man-dir and --info-dir.

I chose --man-path to be consistent with the other options, but in reality, I think all these options specify directories rather than paths (e.g. lists of directories).

jon.

Junio C Hamano wrote:

I was not forgetting it, but you are right that we have an opportunity to be more helpful in that case. (My own MANPATH already includes ~/share/man, but I can see that it is easy to forget to add.)

I am still not very happy about it. The man browser is in a much better position to help: the default MANPATH (at least under Debian; see manpath(5)[1]) is generated by mapping $PATH entries on the fly, and it seems like only an oversight that it deals with directories under /usr but not /home. And it does not thrill me that we would be training people that

	git help git

will cover for the installer's mistakes, while the more conventional

	man git

mechanism (which is also used for other programs installed to $HOME) will not.

I find the "use the right version of help when multiple copies of git" use case compelling enough already. Please don't mind my complaints too much.

Thanks for clarifying. Jonathan

[1] http://man.he.net/man5/manpath

Jonathan Nieder <jrnieder@gmail.com> writes:

Well, is there anything I can do to help your unhappiness about that?

Where is your unhappiness coming from?  Is this your argument?

	'git help' allows distros' oversight with its -m and -i options;
	it discourages distros to get their act together.

I personally do not think punishing users of distros by not helping would be an effective way to encourage distros to help their users, so even though I kind of agree with that statement, I wouldn't conclude that with "therefore, git shouldn't try to be helpful with 'help [-m|-i]'".

Junio C Hamano wrote:

No, my discomfort was not on behalf of distros. It wouldn't do anything to help or hurt distros, since they would be installing to /usr/share/man.

When I said "installers' mistakes", I specifically meant the user that installs manual pages to ~/share/man without setting MANPATH to include that. I agreed that that's an unfortunate thing to happen to anybody, but I didn't think git is the right place to fix it. Because it affects anyone else installing something to $HOME, and as a user I wouldn't _expect_ git to fix it.

What my analysis was missing is that this is not only about the user who runs "git help -m" as a fancy way of running "man git" and expects it to work better (who I still have no sympathy for). It is much more about the user who runs

	git add --help

or chooses Help → Manual in her porcelain, who certainly deserves some documentation whether her MANPATH is set correctly or not.

I also should have remembered v1.5.4-rc0~54 (Let git-help prefer man-pages installed with this version of git, 2007-12-06), which is about showing the manual in /opt/git-next/man in preference to a stale manpage from /opt/git-master/man when running "/opt/git-next/bin/git add --help".

So I was very confused indeed. Sorry to waste your time, and thanks for setting me straight.

These options tell UI programs where git put its documentation, so "Help" actions can show the documentation for *this* version of git without regard to how MANPATH and INFOPATH are set up. Details:

. Each variable tells where documentation is expected to be.  They do
  not indicate whether documentation was actually installed.

. The output of "git --html-path" is an absolute path and can be used
  in "file://$(git --html-path)/git-add.html" to name the HTML file
  documenting a particular command.

. --man-path names a manual page hierarchy (e.g.,
  /home/user/share/man).  Its output can be passed to "man -M" or put
  at the beginning of $MANPATH.

. --info-path names a directory with info files (e.g.,
  /home/user/share/info).  Its output is suitable as an argument to
  "info -d" or for inclusion in $INFOPATH.

Helped-by: Junio C Hamano <gitster@pobox.com>
Signed-off-by: Jonathan Nieder <jrnieder@gmail.com>
---
Sorry for the long tangent.  Maybe a summary can be useful.

 Documentation/git.txt |   12 ++++++------
 1 files changed, 6 insertions(+), 6 deletions(-)

Acked.

On Mon, May 2, 2011 at 4:07 PM, Jonathan Nieder <jrnieder@gmail.com> wrote:

Thanks.