Merge commit '910bf7b1c1e58c1b8dbe2ae7aeb362af5788a932'

Kai Reinhard

22.11.2019 c24c3f945abd2fe4c6780d66e8a46447e13602aa

1
2
3
4
5
6
7
8
9
10
11
12
td.tt {
    white-space: pre-wrap;
    font-family: monospace;
}
td.log-warn, td.log-error {
    color: red;
    font-weight: bold;
}
mark.highlight {
    padding: 0px;
    background-color: yellow;
}