Re: [PATCH 2/3] doc-diff: add --clean mode to remove temporary working gunk

2018-08-31 Thread Eric Sunshine
On Fri, Aug 31, 2018 at 4:01 PM Jeff King wrote: > On Fri, Aug 31, 2018 at 02:33:17AM -0400, Eric Sunshine wrote: > > OPTIONS_SPEC="\ > > doc-diff [options] [-- ] > > +doc-diff (-c|--clean) > > -- > > j=n parallel argument to pass to make > > fforce rebuild; do not rely on cached resul

Re: [PATCH 2/3] doc-diff: add --clean mode to remove temporary working gunk

2018-08-31 Thread Jeff King
On Fri, Aug 31, 2018 at 02:33:17AM -0400, Eric Sunshine wrote: > As part of its operation, doc-diff creates a bunch of temporary > working files and holds onto them in order to speed up subsequent > invocations. These files are never deleted. Moreover, it creates a > temporary working tree (via gi

[PATCH 2/3] doc-diff: add --clean mode to remove temporary working gunk

2018-08-30 Thread Eric Sunshine
As part of its operation, doc-diff creates a bunch of temporary working files and holds onto them in order to speed up subsequent invocations. These files are never deleted. Moreover, it creates a temporary working tree (via git-wortkree) which likewise never gets removed. Without knowing the impl