div.highlight pre {
    font-family: "DejaVu Sans Mono", "Noto Sans Mono", monospace;
}