@charset "utf-8";

* {
    font-family: Georgia, Times, "Times New Roman", serif;
    font-size: 105%;
}

.syntaxhighlighter .gutter {
    display: none;
}

a[href]:after {
    content: none;
}

pre, .syntaxhighlighter * {
    white-space: normal;
}