1 /* XXX Colours. Lots of colours. */
8 border-bottom: solid 1px #ccc;
20 font-family: monospace;
23 background-color: #ddd;
30 font-family: monospace;
34 font-family: monospace;
41 border-bottom: solid 1px #ddd;
51 text-decoration: underline;
59 background-color: #333;
61 border-left: solid 3px #c33;