On Thu, Aug 30, 2018 at 05:04:32AM -0400, Eric Sunshine wrote: > On Thu, Aug 30, 2018 at 3:54 AM Jeff King <[email protected]> wrote: > > Subject: [PATCH] doc-diff: force worktree add > > > > We avoid re-creating our temporary worktree if it's already > > there. But we may run into a situation where the worktree > > has been deleted, but an entry still exists in > > $GIT_DIR/worktrees. > > Can "clean" or "distclean" also be augmented to remove this worktree > (and directory)? I guess that "distclean" would make more sense than > "clean"(?).
I suppose so. I don't think I've _ever_ used distclean, and I only rarely use "clean" (a testament to our Makefile's efforts to accurately track dependencies). I'd usually use "git clean" when I want something pristine (because I don't want to trust the Makefile at all). -Peff
