From 746c02f34a2b5b3f21ffc174f9bb9e199d4a238c Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Mon, 24 Oct 2022 12:26:12 -0400
Subject: [PATCH] Specified font size in VF startup script.

---
 verification/verifast/start-vfide--preprocessed.sh | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/verification/verifast/start-vfide--preprocessed.sh b/verification/verifast/start-vfide--preprocessed.sh
index 73381fe9c..93d47a6fd 100755
--- a/verification/verifast/start-vfide--preprocessed.sh
+++ b/verification/verifast/start-vfide--preprocessed.sh
@@ -13,6 +13,8 @@ PP_SCRIPT_DIR="$START_WD/custom_build_scripts_RP2040"
 PP_SCRIPT="./preprocess_tasks_c.sh"
 PP_TASK_C="$START_WD/preprocessed_files/tasks--pp.c"
 
+FONT_SIZE=16
+
 cd "$PP_SCRIPT_DIR"
 pwd
 ls
@@ -21,4 +23,5 @@ cd "$START_WD"
 
 echo "\n\nPreprocessing script finished\n\n"
 
-"$VF_DIR/bin/vfide" "$PP_TASK_C"
+"$VF_DIR/bin/vfide" "$PP_TASK_C" \
+    -codeFont "$FONT_SIZE" -traceFont "$FONT_SIZE"