16 Jun
2017
16 Jun
'17
2:53 p.m.
How does one choose font for \starttyping? It is apparently different from that of \tt.