From 175ea44edec51111170ba5d6a58931ba749d834d Mon Sep 17 00:00:00 2001
From: quenousimporte <76260127+quenousimporte@users.noreply.github.com>
Date: Sun, 5 Feb 2023 10:46:29 +0100
Subject: [PATCH] added: alternative shortcuts for command palette

---
 main.js | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/main.js b/main.js
index 0b2a11a..74ce98d 100644
--- a/main.js
+++ b/main.js
@@ -2057,6 +2057,10 @@ function mainkeydownhandler()
 		fileindex = Math.max(fileindex, 0);
 		applyfileindex();
 	}
+	else if (event.ctrlKey && event.key == " " || event.key == "F2")
+	{
+		commandpalette();
+	}
 	else
 	{
 		commands.filter(c => c.shortcut)