doc: Make the font bit nices

diff --git a/doc/website-docs.css b/doc/website-docs.css
index 2b605b7684928656749d962c5adc98dee213a6f1..6f4458cc12668235addfa87ecfc393042cb43131 100644 (file)
--- a/doc/website-docs.css
+++ b/doc/website-docs.css
@@ -2,9 +2,16 @@
 
 /* requires global.css, table.css and text.css to be loaded before this file! */
 body {
+  font-family: verdana, sans-serif;
   font-size: 76%;
 }
 
+/* monospace font size fix */
+pre, code, kbd, samp, tt {
+  font-family: monospace,monospace;
+  font-size: 1em;
+}
+
 div.NAVHEADER table {
   margin-left: 0;
 }