From 343851128aed2b91b33d9ebf143429c9acda16cc Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 15 Jul 2024 11:44:17 -0500
Subject: [PATCH] font

---
 .vscode/settings.json | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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"
 }