Re: [PATCH] doc: doc-diff: specify date

[Junio C Hamano <gitster@pobox.com>]

Jeff King <peff@peff.net> writes:

>> >  			GIT_VERSION=omitted \
>> > +			GIT_DATE=1970-01-01 \
>> >  			SOURCE_DATE_EPOCH=0 \
>> >  			DESTDIR="$tmp/installed/$dname+" \
>> >  			install-man &&
>> 
>> I wonder what the existing SOURCE_DATE_EPOCH was trying to do there,
>> though.
>
> It used to be necessary so that we had a reproducible build. Otherwise,
> asciidoc uses the mtime of the file, and diffing two versions would have
> tons of uninteresting date-differences.
>
> After 28fde3a1 I doubt it is necessary, as the header uses $GIT_DATE
> instead (it's possible the mtime may be used elsewhere, but I didn't see
> any spot after grepping a built xml file. And at any rate, if it does
> not produce a visible difference, that is enough for doc-diff).

Thanks for confirming my suspicion.  I guess leaving it there still
would not hurt.  It can be removed whenever somebody motivated
enough comes and shows a well-reasoned patch that explains why it no
longer is necessary ;-)