/* Change the color of deprecated function messages */
.deprecated {
    color: red !important;
    font-weight: bold;
}