common: more hacks to avoid UnicodeErrors in print()