.red {
    color: darkred;
    }

.underline {
    text-decoration: underline;
}

.big {
    font-size: 18px;
    font-weight: bold;
    color: #336699;
}

.highlighted {
    /* Make highlighted text in search results more readable in admonitions */
    background-color: #ec7a00 !important;
}