added shellcmd style
authorhaftmann
Sat, 04 Jun 2005 21:35:20 +0200
changeset 16237 d97b594cba5f
parent 16236 2a6f326ce0ab
child 16238 c1102cdf601f
added shellcmd style
Admin/website/dist/css/isabelle_base.css
--- a/Admin/website/dist/css/isabelle_base.css	Sat Jun 04 20:48:03 2005 +0200
+++ b/Admin/website/dist/css/isabelle_base.css	Sat Jun 04 21:35:20 2005 +0200
@@ -135,8 +135,13 @@
 }
 
 /* shell commands */
+tt.shellcmd {
+    font-family: monospace;
+}
+
 ul.shellcmd {
     background-color: #8080F0;
+    font-family: monospace;
 }
 
 ul.shellcmd li:before {