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

From: Jeff King <peff@peff.net>
Date: May 5, 2023, 01:46 UTC
Message-ID: <20230505014610.GA2366370@coredump.intra.peff.net>
In-Reply-To: <xmqq8re3inn4.fsf@gitster.g>

On Thu, May 04, 2023 at 06:15:59PM -0700, Junio C Hamano wrote:

Show 15 quoted lines

> > diff --git a/Documentation/doc-diff b/Documentation/doc-diff
> > index 1694300e50..554a78a12d 100755
> > --- a/Documentation/doc-diff
> > +++ b/Documentation/doc-diff
> > @@ -153,6 +153,7 @@ render_tree () {
> >  		make -j$parallel -C "$tmp/worktree" \
> >  			$makemanflags \
> >  			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).

-Peff