/* standard OTP style sheet */ body { background: #fefefe; color: #3E4349; font-family: 'goudy old style', 'minion pro', 'bell mt', Georgia, 'Hiragino Mincho Pro', serif; margin: 0; padding: 0; border: 0; overflow: scroll; height: 100%; 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 } .header { background: #222; color: #fefefe } .top { background: #efe } .otp { background: #efe } .erlang { background: #ffe } .otp2 { background: #efe } .app { background: #ffe } a:link { color: blue; text-decoration: none } a:active { color: blue; text-decoration: none } a:visited { color: blue; text-decoration: none } #container { width: 100%; margin: 0; background-color: #fefefe; } #leftnav { position: fixed; float: left; top: 0; bottom: 0; left: 0; width: 300px; overflow:auto; margin: 0; padding: 1px; border-right: 1px solid #ccc; } #content { margin-left: 340px; /* set left value to WidthOfFrameDiv */ } .frontpage { 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) */ } .footer { margin: 15px; /* Magins for inner DIV inside each DIV (to provide padding) */ } span.bold_code { font-family: mono, Courier, monospace; white-space: pre; font-weight: bold } span.code { font-family: mono, Courier, monospace; white-space: pre; font-weight: normal } .note, .warning, .do, .dont { border: 1px solid #495057; margin: 1em 3em; } .note .label { background-color: #2b8a3e; color: #fefefe; font-weight: bold; padding: 5px 10px; } .note .content { background: #f8f9fa; line-height: 120%; font-size: 90%; padding: 0.5em 1em; } .warning .label { background: #c92a2a; color: #fefefe; font-weight: bold; padding: 5px 10px; } .warning .content { background-color: #f8f9fa; border: 1px solid #dee2e6; line-height: 120%; font-size: 90%; padding: 0.5em 1em; } .do .label { background: #30d42a; color: #fefefe; font-weight: bold; padding: 5px 10px; } .do .content { background: #eafeea; color: #3E4349; line-height: 120%; font-size: 90%; padding: 5px 10px; } .dont .label { background: #C00; color: #fefefe; font-weight: bold; padding: 5px 10px; } .dont .content { background: #FFF0F0; color: #3E4349; line-height: 120%; font-size: 90%; padding: 5px 10px; } .quote { font-style: italic } .example { background-color:#f1f3f5; border: 1px solid #dee2e6; padding: 0.5em 1em; } .extrafrontpageinfo { color: #C00; font-weight: bold; font-size: 120%; } pre { font-family: mono, Courier, monospace; font-weight: normal } .REFBODY { margin-left: 13mm } .REFTYPES { margin-left: 8mm } footer { }