Re: [PATCH] doc/Makefile: remove tmp-doc-diff on "make clean"

From: Jeff King <peff@peff.net>
Date: Aug 30, 2018, 20:52 UTC
Message-ID: <20180830205208.GB27399@sigill.intra.peff.net>
In-Reply-To: <CAPig+cRXEegGwm3QiyEZqkVN1NYv5xAAYRuAKHUE8n-g9m6jqw@mail.gmail.com>

On Thu, Aug 30, 2018 at 04:34:43PM -0400, Eric Sunshine wrote:

Show 22 quoted lines

> On Thu, Aug 30, 2018 at 3:55 PM Jeff King <peff@peff.net> wrote:
> > The tmp-doc-diff directory isn't strictly a build product of
> > the Makefile, since it's only present if you manually run
> > the doc-diff script.  But anybody running "make clean" would
> > probably want it to go away.
> >
> > Suggested-by: Eric Sunshine <sunshine@sunshineco.com>
> > Signed-off-by: Jeff King <peff@peff.net>
> > ---
> > diff --git a/Documentation/Makefile b/Documentation/Makefile
> > @@ -332,6 +332,7 @@ clean:
> >         $(RM) manpage-base-url.xsl
> > +       $(RM) -r tmp-doc-diff
> 
> Taking into consideration that people might be surprised and alarmed
> to find "git worktree list" showing a worktree they didn't explicitly
> create, would it make sense to do something like this?
> 
> clean:
>     ...
>     -git worktree remove -f tmp-doc-diff 2>/dev/null
>     $(RM) -r tmp-doc-diff

Seems reasonable. Again, I don't have a strong feeling. It's a little strange to me for the Makefile to be touching bits outside of the actual working tree. But then, creating a separate worktree in the first place is perhaps a little weird.

I dunno. Maybe you are right that worktrees are a bad fit here.

-Peff