On 2014-09-29 18:28, John Regehr wrote:
No particular rush. Thanks. Also I'd say merge the floating-point branch any time you want. John
Yes, Thanks. - Yang