-
Phil Sutter authored
We commonly use bold font for terminals and italic for non-terminals. Signed-off-by: Phil Sutter <phil@nwl.cc>
d890144e
We commonly use bold font for terminals and italic for non-terminals.
Signed-off-by: Phil Sutter <phil@nwl.cc>