summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/generic/tex-refs/tex-refs.css
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/doc/generic/tex-refs/tex-refs.css')
-rw-r--r--Master/texmf-dist/doc/generic/tex-refs/tex-refs.css124
1 files changed, 124 insertions, 0 deletions
diff --git a/Master/texmf-dist/doc/generic/tex-refs/tex-refs.css b/Master/texmf-dist/doc/generic/tex-refs/tex-refs.css
new file mode 100644
index 00000000000..c4d1e1bdc53
--- /dev/null
+++ b/Master/texmf-dist/doc/generic/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;
+}
+