On Thu, Aug 30, 2018 at 04:34:43PM -0400, Eric Sunshine wrote:
On Thu, Aug 30, 2018 at 3:55 PM Jeff King [off-list ref] wrote:
quoted
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 <redacted>
Signed-off-by: Jeff King <redacted>
---
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