|Subject:||Re: [PATCH] "make dist" did not depend on $(BUILT_SOURCES)|
|Date:||Tue, 28 Nov 2017 19:43:15 -0800|
On Tue, Nov 28, 2017 at 12:01 PM, Mathieu Lirzin <address@hidden> 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.
|[Prev in Thread]||Current Thread||[Next in Thread]|