From 351cdc3afd51f96edd26d94b3bbc52e0e1d94a7b Mon Sep 17 00:00:00 2001
From: traxys <quentin@familleboyer.net>
Date: Wed, 26 Jul 2023 09:50:46 +0200
Subject: [PATCH] personal-gui: Allow terminal fonts to be floating numbers

---
 personal-gui/wm/terminal/default.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/personal-gui/wm/terminal/default.nix b/personal-gui/wm/terminal/default.nix
index b68b302..3271605 100644
--- a/personal-gui/wm/terminal/default.nix
+++ b/personal-gui/wm/terminal/default.nix
@@ -57,7 +57,7 @@ in {
       };
       font = {
         size = mkOption {
-          type = types.int;
+          type = types.number;
           default = 12;
           description = "terminal font size";
         };