--- a/model/extra-dm.css Wed Apr 25 10:21:17 2012 +0200
+++ b/model/extra-dm.css Wed Apr 25 10:22:41 2012 +0200
@@ -395,6 +395,7 @@
font-size:130%;
font-family: monospace;
content: ")";
+}
div[class="grammar"] span[class="group"]:before {
font-weight: normal;
--- a/model/extra.css Wed Apr 25 10:21:17 2012 +0200
+++ b/model/extra.css Wed Apr 25 10:22:41 2012 +0200
@@ -372,6 +372,7 @@
font-size:130%;
font-family: monospace;
content: ")";
+}
div[class="grammar"] span[class="group"]:before {
font-weight: normal;