chiark / gitweb /
dot/putty-defaults: Express the font name in a more modern way.