X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2Fpintos.css;h=0af878f2f63d52ad36613b21ee1fdb1e7daaaa7d;hb=3edcfedb8e62970f3293fa676b6691f8658c3c11;hp=f904001d7a3d9188471ec59b2a360872db44102f;hpb=615bf3b3d2a8573ed6fb9ddc0055745e163ac999;p=pintos-anon

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;