aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorHenrik Nord <[email protected]>2012-02-16 12:09:33 +0100
committerHenrik Nord <[email protected]>2012-02-16 12:09:43 +0100
commitd53717a4fde3313819b9fc3493bb223f5775fe6c (patch)
treeadf14f3bb5a17a7853636ac38025a2c26ccef3da
parent815645f54acd5876211eda76b7299d827e553bfe (diff)
parentae32e948df219825ff1e9e214c15733017a9fed7 (diff)
downloadotp-d53717a4fde3313819b9fc3493bb223f5775fe6c.tar.gz
otp-d53717a4fde3313819b9fc3493bb223f5775fe6c.tar.bz2
otp-d53717a4fde3313819b9fc3493bb223f5775fe6c.zip
Merge branch 'rj/doc-monospace-css' into maint
* rj/doc-monospace-css: Set `font-family: Courier, monospace' in OTP doc CSS OTP-9918
-rw-r--r--lib/erl_docgen/priv/css/otp_doc.css29
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 { }