On Thu, Oct 4, 2012 at 2:14 PM, Lawrence Crowl <crowl@googlers.com> wrote: > So, Jan Hubicka requested and approved the current spelling. > What now? I don't think we should hold this up. The names Jan requested seem reasonable enough. We seem to be running in circles here. Diego.