# HG changeset patch
# User haftmann
# Date 1117913720 -7200
# Node ID d97b594cba5f0ccb27c1a239dc017c48c9a6addd
# Parent  2a6f326ce0aba480be4a89434f3ecc25df217b65
added shellcmd style

diff -r 2a6f326ce0ab -r d97b594cba5f 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 {