> On Dec 18, 2019, at 6:19 PM, Daniel D. Daugherty <daniel.daugherty at oracle.com> wrote: > > Thanks! Should I push this fix in hopes that it is the only merge > error or should I do a Linux test build? I think go ahead and push.