From: Ben Pfaff Date: Sat, 25 Jun 2005 03:44:25 +0000 (+0000) Subject: Make use boldface. X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=589006d404af818edc3996079ca077c85727db3b;p=pintos-anon Make use boldface. --- diff --git a/doc/pintos.css b/doc/pintos.css index f904001..0af878f 100644 --- a/doc/pintos.css +++ b/doc/pintos.css @@ -46,6 +46,9 @@ html { tt, code { font-family: sans-serif } +b, strong { + font-weight: bold +} a:link { color: blue;