![](https://secure.gravatar.com/avatar/d558f7d2c62b984d42b1e276bbdfc2c7.jpg?s=120&d=mm&r=g)
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.