diff options
Diffstat (limited to 'ide/.coqide-gtk2rc')
| -rw-r--r-- | ide/.coqide-gtk2rc | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/.coqide-gtk2rc b/ide/.coqide-gtk2rc index da2c5d929e..11099742e2 100644 --- a/ide/.coqide-gtk2rc +++ b/ide/.coqide-gtk2rc @@ -4,6 +4,7 @@ # for a complete set of options # To set the font of the text windows, edit the .coqiderc file through the menus. +gtk-key-theme-name = "Emacs" binding "text" { bind "<ctrl>k" { "set-anchor" () @@ -11,10 +12,10 @@ binding "text" { "cut-clipboard" () } bind "<ctrl>w" { "cut-clipboard" () } - bind "<ctrl>x" { } - bind "F13" {"insert-at-cursor" ("∀")} - bind "F14" {"insert-at-cursor" ("∃")} +# For UTF-8 inputs ! + bind "F11" {"insert-at-cursor" ("∀")} + bind "F12" {"insert-at-cursor" ("∃")} } class "GtkTextView" binding "text" @@ -35,4 +36,3 @@ font_name = "Monospace 10" } widget "*location*" style "location" -gtk-key-theme-name = "Emacs" |