fix: gtd control key (marimo-team#1467)

PatrickCleary · May 23, 2024 · dee0e0d · dee0e0d
1 parent fc53164
commit dee0e0d
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/frontend/src/core/codemirror/go-to-definition/underline.ts b/frontend/src/core/codemirror/go-to-definition/underline.ts
@@ -108,7 +108,7 @@ class MetaUnderlineVariablePlugin {
  };
 
  private keydown = (event: KeyboardEvent) => {
- if (event.key === "Meta" || event.key === "Ctrl") {
+ if (event.key === "Meta" || event.key === "Control") {
  this.commandKey = true;
  }
  };
@@ -133,7 +133,7 @@ class MetaUnderlineVariablePlugin {
  };
 
  private keyup = (event: KeyboardEvent) => {
- if (event.key === "Meta" || event.key === "Ctrl") {
+ if (event.key === "Meta" || event.key === "Control") {
  this.commandKey = false;
  this.clearUnderline();
  }