Switch to unified view

a/website/styles/style.css b/website/styles/style.css
...
...
63
h3 {
63
h3 {
64
  font-weight:          bold;
64
  font-weight:          bold;
65
  font-size:            100%;
65
  font-size:            100%;
66
  padding-top: 1em;
66
  padding-top: 1em;
67
}
67
}
68
69
p.indexthumb {
68
p.indexthumb {
70
    margin-left: 1em;
69
    margin-left: 1em;
71
}
70
}
72
.guimenu, .guimenuitem, .guisubmenu,
71
.guimenu, .guimenuitem, .guisubmenu,
73
.guilabel, .interface, .guibutton,
72
.guilabel, .interface, .guibutton,
74
.shortcut, .shortcut .keycap {
73
.shortcut, .shortcut .keycap {
75
    background-color: #F0F0F0;
74
    background-color: #F0F0F0;
76
    font-family: monospace;
75
    font-family: monospace;
76
}
77
78
p.remark {
79
    color: #888888;
80
    font-size: 80%;
81
    font-style: italic;
82
    margin-left: 4em;
83
    margin-right: 4em;
84
}
85
div.news {
86
    font-size: 80%;
77
}
87
}
78
.application {
88
.application {
79
    font-weight: bold;
89
    font-weight: bold;
80
}
90
}
81
.literal {
91
.literal {