From: Junio C Hamano <gitster@pobox.com>
Date: Wed, 06 Jun 2012 21:07:03 GMT
Subject: Re: [PATCH] Add the DEFAULT_HELP_FORMAT option to Makefile
Message-ID: <7vk3zkkv48.fsf@alter.siamese.dyndns.org>
In-Reply-To: <4FCFBC9C.6010501@lyx.org>

Vincent van Ravesteijn <vfr@lyx.org> writes:

> Op 6-6-2012 21:06, Junio C Hamano schreef:
>> I think the choices of PAGER and EDITOR share the same problem, but
>> shouldn't this choice recorded in GIT-BUILD-OPTIONS in some way?
>
> I don't know. The only place I know where GIT-BUILD-OPTIONS  is used
> is in the test suite. The test suite runs fine with the patches.

Actually what I had in mind was GIT-CFLAGS which makes sure that we
rebuild things when compilation options change, but ALL_CFLAGS is
covered already so there is no problem.

Thanks for a sanity check.