From d619c92a8ffe185148aa5e3acce42aa0f9b2451b Mon Sep 17 00:00:00 2001
From: Julien Palard <julien@palard.fr>
Date: Tue, 25 Sep 2018 19:30:27 +0200
Subject: [PATCH] Alias to change font size.

---
 .bashrc | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/.bashrc b/.bashrc
index a7fffb2..05fa866 100644
--- a/.bashrc
+++ b/.bashrc
@@ -144,3 +144,8 @@ dotfiles()
     rm -f "$HOME/.git-prompt.sh"
     wget -q -O "$HOME/.git-prompt.sh" https://raw.githubusercontent.com/git/git/master/contrib/completion/git-prompt.sh
 }
+
+fontsize()
+{
+    printf '\33]50;%s\007' "xft:LiberationMono:size=$1"
+}