Blame SOURCES/odoc_style.css

0f45c0
body { padding: 0px 20px 0px 26px; background: #ffffff; color: #000000; font-family: Verdana, Arial, Helvetica, sans-serif; font-size: 90%; }
0f45c0
h1 { padding : 5px 0px 5px 0px; font-size : 16pt; font-weight : normal; background-color : #E0E0FF }
0f45c0
h6 { padding : 5px 0px 5px 20px; font-size : 16pt; font-weight : normal; background-color : #E0E0FF }
0f45c0
a:link, a:visited, a:active { text-decoration: none; }
0f45c0
a:link { color: #000077; }
0f45c0
a:visited { color: #000077; }
0f45c0
a:hover { color: #cc9900; }
0f45c0
.keyword { font-weight : bold ; color : Blue }
0f45c0
.keywordsign { color : #606060 }
0f45c0
.superscript { font-size : 4 }
0f45c0
.subscript { font-size : 4 }
0f45c0
.comment { color : #606060 }
0f45c0
.constructor { color : #808080; }
0f45c0
.type { color : #606060 }
0f45c0
.string { color : Red }
0f45c0
.warning { color : Red ; font-weight : bold }
0f45c0
.info { margin-left : 3em; margin-right : 3em }
0f45c0
.code { color : #606060 ; }
0f45c0
.title1 { font-size : 16pt ; background-color : #E0E0E0 }
0f45c0
.title2 { font-size : 16pt ; background-color : #E0E0E0 }
0f45c0
.title3 { font-size : 16pt ; background-color : #E0E0E0 }
0f45c0
.title4 { font-size : 16pt ; background-color : #E0E0E0 }
0f45c0
.title5 { font-size : 16pt ; background-color : #E0E0E0 }
0f45c0
.title6 { font-size : 16pt ; background-color : #E0E0E0; }