On Wed, Jul 15, 2015 at 5:58 PM, Diego Novillo <dnovillo at google.com> wrote: > On Wed, Jul 15, 2015 at 7:13 PM, Alexey Samsonov <vonosmas at gmail.com> wrote: >> I'm pretty sure we should, but let Diego verify that. > > Yes, please. Thanks for the fix! Merged in r242405. Thanks, Hans