On Sun, Oct 07, 2012 at 01:39:32PM -0700, Junio C Hamano wrote:

> By default, "make doc" generates the manpages and htmldocs in the
> Documentation directory, but you may want to change this depending
> on the target environment, e.g. to include 'pdf'.  Introduce a new
> Makefile variable DEFAULT_DOC_TARGET to allow customizing this.

Makes sense (we have DEFAULT_TEST_TARGET for similar reasons).

> The primary motivation is to let us check documentation patches with
>     $ DEFAULT_DOC_TARGET=git-push.1 make doc

Wouldn't it be just as easy to say:

  $ make -C Documentation git-push.1


> but it is not so far-fetched to imagine that Windows users may want to
> omit manpages with
>     $ DEFAULT_DOC_TARGET=html make doc

That use case makes a lot more sense to me (or more likely setting it in

>  Makefile | 12 ++++++++++--
>  1 file changed, 10 insertions(+), 2 deletions(-)

No change to Documentation/Makefile? So this will work:

  $ echo DEFAULT_DOC_TARGET=html >config.mak
  $ make doc

but this will not:

  $ cd Documentation
  $ make

Why not do it like this:

diff --git a/Documentation/Makefile b/Documentation/Makefile
index 267dfe1..ca10313 100644
--- a/Documentation/Makefile
+++ b/Documentation/Makefile
@@ -152,7 +152,8 @@ endif
-all: html man
 html: $(DOC_HTML)

which covers both cases? That is also how we handle DEFAULT_TEST_TARGET.

To unsubscribe from this list: send the line "unsubscribe git" in
the body of a message to majord...@vger.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html

Reply via email to