keystroke '\\': 'agda-mode:input-symbol' does not work for some user (#…

…10), another keystroke 'alt-/' will be supported
banacorn · May 28, 2015 · 35380ed · 35380ed
1 parent e770130
commit 35380ed
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/keymaps/agda-mode.cson b/keymaps/agda-mode.cson
@@ -23,3 +23,4 @@
   'ctrl-c ctrl-a': 'agda-mode:auto'
   'ctrl-c ctrl-n': 'agda-mode:normalize'
   '\\': 'agda-mode:input-symbol'
+  'alt-/': 'agda-mode:input-symbol'