George Garvey wrote: > It appears that the font cannot be different in different instances >of Terminal, nor can it be set on the command line. Did I just miss >something, or is really not implemented? > > You missed something: right-click on the Terminal, select "preferences", then "Appearance"... right on the top sofar