Merge branch 'rj/doc-monospace-css' into maint

* rj/doc-monospace-css:
  Set `font-family: Courier, monospace' in OTP doc CSS

OTP-9918

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       { }