/* extra style sheet for doxygen-generated pages */
code,pre
{
    font-size:110%;
    background-color:#eee;
}