--- a/model/extra.css Sun Jul 08 23:00:37 2012 +0100 +++ b/model/extra.css Sun Jul 08 23:11:14 2012 +0100 @@ -232,7 +232,7 @@ padding-top: 1ex; padding-bottom: 0.6ex; border: 1px dashed #2f6fab; - font-size: 80%; + font-size: 95%; } .nonterminal { font-weight: bold;