add numpad-enter key #212

leanprover-community · Apr 17, 2024 · 62f1fb8 · 62f1fb8
1 parent 848b2cd
commit 62f1fb8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/client/src/components/infoview/typewriter.tsx b/client/src/components/infoview/typewriter.tsx
@@ -229,7 +229,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
     if (!oneLineEditor) return
     // Run command when pressing enter
     const l = oneLineEditor.onKeyUp((ev) => {
-      if (ev.code === "Enter") {
+      if (ev.code === "Enter" || ev.code === "NumpadEnter") {
         runCommand()
       }
     })