-
Notifications
You must be signed in to change notification settings - Fork 1.2k
/
doxygen_extra.css
132 lines (98 loc) · 2.14 KB
/
doxygen_extra.css
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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
/* s3://drake-web/fonts/stylesheet.css */
@import url('https://dmn3132s4wr9m.cloudfront.net/fonts/stylesheet.css');
/* user agent html.css */
tt, code, kbd, samp {
font-family: 'DejaVu Sans Mono', monospace;
}
pre, xmp, plaintext, listing {
font-family: 'DejaVu Sans Mono', monospace;
}
/* /tabs.css */
.sm-dox a, .sm-dox a:focus, .sm-dox a:hover, .sm-dox a:active {
font-family: 'DejaVu Sans', sans-serif;
}
/* /navtree.css */
#nav-tree .label {
font-family: 'DejaVu Sans', sans-serif;
}
/* /search/search.css */
.SelectItem {
font-family: 'DejaVu Sans', sans-serif;
}
.SRSymbol {
font-family: 'DejaVu Sans', sans-serif;
}
/* /doxygen.css */
body, table, div, p, dl {
font-family: 'DejaVu Sans', sans-serif;
}
p.reference, p.definition {
font-family: 'DejaVu Sans', sans-serif;
}
.title {
font-family: 'DejaVu Sans', sans-serif;
}
pre.fragment {
font-family: 'DejaVu Sans Mono', monospace;
}
div.line {
font-family: 'DejaVu Sans Mono', monospace;
}
div.groupText {
font-style: inherit;
}
.overload {
font-family: 'DejaVu Sans Mono', monospace;
}
.params .paramdir {
font-family: 'DejaVu Sans Mono', monospace;
}
.icon {
font-family: 'DejaVu Sans', sans-serif;
}
table.directory {
font-family: 'DejaVu Sans', sans-serif;
}
.navpath li.navelem a {
font-family: 'DejaVu Sans', sans-serif;
}
#projectname {
font-family: 'DejaVu Sans', sans-serif;
}
#projectbrief {
font-family: 'DejaVu Sans', sans-serif;
}
#projectnumber {
font-family: 'DejaVu Sans', sans-serif;
}
div.toc li {
font-family: 'DejaVu Sans', sans-serif;
}
div.toc h3 {
font-family: 'DejaVu Sans', sans-serif;
}
#powerTip div {
font-family: 'DejaVu Sans', sans-serif;
}
/* Custom CSS */
pre.unicode-art {
font-family: 'DejaVu Sans Mono', monospace;
line-height: 1em;
}
/* Place the duckduckgo.com search box in the upper right. */
#DDGSearch {
white-space : nowrap;
float: none;
margin-top: 0px;
top: 8px;
right: 20px;
width: 200px;
height: 24px;
z-index: 102;
display: inline;
position: absolute;
}
/* Adjust the built-in "Quick jump" search to make room for theh DDGSearch. */
#MSearchBox {
top: 60px;
}