diff options
author | Ricardo Catalinas Jiménez <[email protected]> | 2012-01-14 18:26:50 +0100 |
---|---|---|
committer | Ricardo Catalinas Jiménez <[email protected]> | 2012-02-04 14:49:07 +0100 |
commit | ae32e948df219825ff1e9e214c15733017a9fed7 (patch) | |
tree | eb158c569220342954148ffebdb84ca43ad96e0d /lib/erl_docgen/priv | |
parent | ab2ba6f1b0713fbe5c78f67aeefb73ffc006e995 (diff) | |
download | otp-ae32e948df219825ff1e9e214c15733017a9fed7.tar.gz otp-ae32e948df219825ff1e9e214c15733017a9fed7.tar.bz2 otp-ae32e948df219825ff1e9e214c15733017a9fed7.zip |
Set `font-family: Courier, monospace' in OTP doc CSS
This should be much better for everybody, I left Courier as the primary
original font and also added monospace as secondary for people like me
which in Linux haven't it installed.
It should be more pleasant to read typespecs and code examples. Also
adds minor cosmetic changes to the CSS.
Diffstat (limited to 'lib/erl_docgen/priv')
-rw-r--r-- | lib/erl_docgen/priv/css/otp_doc.css | 29 |
1 files changed, 11 insertions, 18 deletions
diff --git a/lib/erl_docgen/priv/css/otp_doc.css b/lib/erl_docgen/priv/css/otp_doc.css index 97d8c2df74..c56de378f4 100644 --- a/lib/erl_docgen/priv/css/otp_doc.css +++ b/lib/erl_docgen/priv/css/otp_doc.css @@ -1,6 +1,5 @@ - - -body { +/* standard OTP style sheet */ +body { background: white; font-family: Verdana, Arial, Helvetica, sans-serif; margin: 0; @@ -11,7 +10,6 @@ body { max-height: 100%; } - th { font-family: Verdana, Arial, Helvetica, sans-serif } td { font-family: Verdana, Arial, Helvetica, sans-serif } p { font-family: Verdana, Arial, Helvetica, sans-serif } @@ -33,8 +31,7 @@ a:visited { color: blue; text-decoration: none } background-color: #fff; } - -#leftnav { +#leftnav { position: fixed; float: left; top: 0; @@ -47,8 +44,7 @@ a:visited { color: blue; text-decoration: none } border-right: 1px solid red; } - -#content { +#content { margin-left: 240px; /* set left value to WidthOfFrameDiv */ } @@ -57,7 +53,6 @@ a:visited { color: blue; text-decoration: none } padding-top: 50px; /* Magins for inner DIV inside each DIV (to provide padding) */ } - .innertube { margin: 15px; /* Magins for inner DIV inside each DIV (to provide padding) */ @@ -66,16 +61,15 @@ a:visited { color: blue; text-decoration: none } .footer { margin: 15px; /* Magins for inner DIV inside each DIV (to provide padding) */ - } -span.bold_code { font-family: courier;font-weight: bold} -span.code { font-family: courier;font-weight: normal} + +span.bold_code { font-family: Courier, monospace; font-weight: bold } +span.code { font-family: Courier, monospace; font-weight: normal } .note, .warning { border: solid black 1px; margin: 1em 3em; } - .note .label { background: #30d42a; color: white; @@ -102,16 +96,15 @@ span.code { font-family: courier;font-weight: normal} font-size: 90%; padding: 5px 10px; } - -.example { +.example { background-color:#eeeeff; padding: 0px 10px; -} +} -pre { font-family: courier; font-weight: normal } +pre { font-family: Courier, monospace; font-weight: normal } .REFBODY { margin-left: 13mm } .REFTYPES { margin-left: 8mm } -footer { } +footer { } |