Fix font family in code snippet (#9334)

master
Florian Angeletti 2020-02-27 09:29:53 +01:00 committed by GitHub
parent 4823934182
commit 1fd6dc077d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions

View File

@ -109,7 +109,7 @@
\newstyle{div.ocaml .pre}{
white-space: pre;
font-family:mono;
font-family: monospace;
}