Yury Gribov Thu, 19 Dec 2013 06:51:18 -0800
The patch is OK. Feel free to submit now, if you want.
Thanks. Done in r206116. -Y