On Wed, Feb 14, 2018 at 13:13:09 -0800, Richard Henderson wrote: > On 02/14/2018 11:52 AM, Emilio G. Cota wrote: > > Should I send those patches to the list, or let Michael squash their > > changes? > > That's up to you, I guess. I don't mind if it goes in before or after merge.
OK, will send to the list once the merge is complete. Thanks, Emilio