font
This commit is contained in:
parent
02c0455505
commit
343851128a
1 changed files with 2 additions and 1 deletions
3
.vscode/settings.json
vendored
3
.vscode/settings.json
vendored
|
@ -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"
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue