On Sat, 2020-01-04 at 20:36 -0500, Dmitry Goncharov wrote: > On Sat, Jan 4, 2020 at 3:23 PM Paul Smith <psm...@gnu.org> wrote: > > Thanks, I did something similar to this but not quite the same. > Have you pushed?
I have now.
- make-4.2.93 p... Dmitry Goncharov via Bug reports and discussion for GNU make
- Re: make... Paul Smith
- Re: ... Dmitry Goncharov via Bug reports and discussion for GNU make
- ... Paul Smith
