On Thu, Oct 4, 2012 at 2:14 PM, Lawrence Crowl <cr...@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.
