diff --git a/.vscode/settings.json b/.vscode/settings.json index e8abc14..5c606e0 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -6,5 +6,6 @@ "agdaMode.connection.commandLineOptions": "--rewriting --without-K", "search.exclude": { "src/CubicalHott/**": true - } + }, + "editor.fontFamily": "'PragmataPro Mono Liga', 'Droid Sans Mono', 'monospace', monospace" }