In set.mm, should we use "Jeff Hankins" vs. "Jeffrey Hankins"?
I think every person should have a unique name in the database, and this is an exception. "Jeffrey Hankins" is what is listed at the front, but "Jeff Hankins" is what is almost always used. I'd prefer a response from M. Hankins, but I don't know if he reads this mailing list. --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1iIhfe-0007zF-Hm%40rmmprod07.runbox.
