diff options
Diffstat (limited to 'Master/texmf-doc/doc/english/tex-refs/tex-refs.css')
-rw-r--r-- | Master/texmf-doc/doc/english/tex-refs/tex-refs.css | 124 |
1 files changed, 124 insertions, 0 deletions
diff --git a/Master/texmf-doc/doc/english/tex-refs/tex-refs.css b/Master/texmf-doc/doc/english/tex-refs/tex-refs.css new file mode 100644 index 00000000000..c4d1e1bdc53 --- /dev/null +++ b/Master/texmf-doc/doc/english/tex-refs/tex-refs.css @@ -0,0 +1,124 @@ +/* $Id: tex-refs.css 120 2004-03-26 20:19:43Z mw $ */ + +body { background-color: whitesmoke; + } + +h1.title { background-color: gainsboro; + text-align: center; + font-family: sans-serif; + color: black; + } + +h2.title { background-color: gainsboro; + font-family: sans-serif; + color: black; + } + +h3.title { background-color: gainsboro; + font-family: sans-serif; + color: black; + } + +h4.title { background-color: gainsboro; + font-family: sans-serif; + color: black; + } +h5.title { background-color: gainsboro; + font-family: sans-serif; +/* font-size: small; */ + color: black; + } +h6.title { background-color: gainsboro; + font-family: sans-serif; +/* font-size: x-small; */ + font-size: small; + color: black; + } +span.title { background-color: gainsboro; + font-family: sans-serif; +/* font-size: x-small; */ + font-size: small; + color: black; + } + +.title { background-color: gainsboro; + font-family: sans-serif; + } + +.authorgroup { + background-color: #EEEEEE + } + +.copyright { + } + +.legalnotice { + } + +.revhistory { + } + +.abstract { + margin-top: 1em + } + +.toc { + } + +.itemizedlist { + } + +.orderedlist { + } + +.variablelist { + } + +.term { background-color: #EFEFEF + } + +pre.programlisting +{ + background-color: #E0E0E0; + border: thin solid gray; + margin-top: 1.33ex; + margin-bottom: 1.33ex; +} + + +.footer-date { font-size: xx-small; + font-family: monospace; + } + + +#customheader, #customfooter +{ + /* list of fonts provides fallbacks if a font is not present */ + font-family: Verdana, Arial, Helvetica, Sans-Serif; + /* font size, relative to body font size */ + font-size: 80%; + + /* line height, relative to body font size */ + line-height: 200%; + + text-align: center; + vertical-align: middle; + color: #fff; + background-color: #009; +} + +/* leave more space between last paragraph and footer */ +/* some browser do not add up the bottom margin of the prior element */ +/* and the top margin of the footer */ +#customfooter { + margin-top: 15px; +} + +/* define special font for logo */ +/* list of fonts provides fallbacks in case selected fonts are not present +*/ +.logo +{ + font-family: Lucida Console, Verdana, Arial, Sans-Serif; +} + |