1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
body { margin-left:2%; margin-right:2%; font-family:serif; }
.toc, .list-of-tables, .list-of-examples { font-family:sans-serif; }
h1, h2, h3, h4, h5, h6 { font-family:sans-serif; }
p { text-align:justify; }
div.table p.title, div.example p.title { font-size:smaller; font-family:sans-serif; }
.email, .email a { font-family:monospace; }
div.table-contents table, div.informaltable table { border-collapse:collapse; border:1px solid #c0c0c0; }
div.table-contents table td, div.informaltable td, div.table-contents table th, div.informaltable table th { padding:5px; text-align:left; }
div.table-contents table th, div.informaltable table th {
font-family:sans-serif;
background:#d0d0d0;
font-weight:bold;
vertical-align:top;
}
div.cmdsynopsis { border-left:1px solid #707070; padding-left: 1em; }
li div.cmdsynopsis { border-left:none; padding-left:0px; }
li p { margin: 0; }
pre.screen, div.note { border:1px solid #c0c0c0; margin-left:2%; margin-right:2%; }
pre.screen { color: #ffffff; background:#000000; padding: 0.5em; }
div.note { background:#ffff80; padding: 0.5em; }
div.example p.title { margin-left:2%; }
div.note h3 { font-size:small; font-style:italic; font-variant: small-caps; }
div.note h3:after { content: ":" }
div.note { margin-bottom: 5px; }
div.literallayout, .command { font-family: monospace; font-weight: normal; }
.command strong { font-weight: normal; }
tr { vertical-align: top; }
.comment { color:#00c000; }
code.literal { background: #f0f0f0; color: #000000; }
span.indicator { background: #000060; color: #ffffff; }
span.highlight { background: #404040; color: #ffffff; }
span.reverse { background: #ffffff; color: #000000; }
|
