Re: [PATCH] "make dist" did not depend on $(BUILT_SOURCES)

[Jim Meyering]

On Tue, Nov 28, 2017 at 12:01 PM, Mathieu Lirzin <m...@gnu.org> wrote:
> Hello Jim,
...
>>
>> Here's the patch I expect to push to master:
...
>
> OK to push.

Thanks. Pushed.
I have also removed the micro branch.