On Tue, 2018-06-05 at 20:18 +0100, Richard Sandiford wrote: > > This still has the change from "floating-point" to "floating point", > but "floating-point" preferred. > > Thanks, > Richard
You are right, I missed that. I haven't checked in the patch yet though so I will fix that before doing the checkin. Steve Ellcey sell...@cavium.com
