web-tools/web/_static/local/font.css


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

a.a-hover-red {
  color: inherit;
}

a.a-hover-red:hover {
  color: #cc0000 !important;
  text-decoration: none;
}

html,
body,
.tooltip,
.popover {
  font-family: 'DejaVuSans';
}

pre,
code,
kbd,
samp,
.text-monospace {
  font-family: 'DejaVuSansMono';
}