File tree 2 files changed +56
-1
lines changed
2 files changed +56
-1
lines changed Original file line number Diff line number Diff line change
1
+ code {
2
+ color : red;
3
+ background-color : WhiteSmoke;
4
+ border-style : solid;
5
+ border-width : 1px ;
6
+ border-color : LightGrey;
7
+ padding : 1px 4px ;
8
+ }
9
+
10
+ h1 {
11
+ font-size : 1.3em ;
12
+ margin : 0.9em 0 ;
13
+ }
14
+
15
+ h2 {
16
+ font-size : 1.2em ;
17
+ margin : 0.6em 0 ;
18
+ }
19
+
20
+ h3 {
21
+ font-size : 1.1em ;
22
+ margin : 0.3em 0 ;
23
+ }
24
+
25
+ pre .fragment , div .fragment {
26
+ padding : 5px ;
27
+ margin-left : 10px ;
28
+ }
29
+
30
+
31
+ a {
32
+ color : # CA7900 ;
33
+ }
34
+
35
+ .contents a : visited {
36
+ color : # 6237a8 ;
37
+ }
38
+
39
+ # nav-tree .label {
40
+ font-weight : bold;
41
+ font-size : 1.1em ;
42
+ }
43
+
44
+ # nav-tree a {
45
+ color : MidnightBlue;
46
+ }
47
+
48
+ # nav-tree .selected a {
49
+ padding : 0.5em ;
50
+ }
51
+
52
+ # nav-tree .item {
53
+ font-size : 1.1em ;
54
+ padding : 0.2em ;
55
+ }
Original file line number Diff line number Diff line change @@ -1133,7 +1133,7 @@ HTML_STYLESHEET =
1133
1133
# list). For an example see the documentation.
1134
1134
# This tag requires that the tag GENERATE_HTML is set to YES.
1135
1135
1136
- HTML_EXTRA_STYLESHEET =
1136
+ HTML_EXTRA_STYLESHEET = ../doc/assets/cbmc_style.css
1137
1137
1138
1138
# The HTML_EXTRA_FILES tag can be used to specify one or more extra images or
1139
1139
# other source files which should be copied to the HTML output directory. Note
You can’t perform that action at this time.
0 commit comments