diff options
Diffstat (limited to 'ide/.coqide-gtk2rc')
| -rw-r--r-- | ide/.coqide-gtk2rc | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/.coqide-gtk2rc b/ide/.coqide-gtk2rc index 7a74a469d..11c53dad2 100644 --- a/ide/.coqide-gtk2rc +++ b/ide/.coqide-gtk2rc @@ -17,8 +17,8 @@ binding "text" { bind "<ctrl>w" { "cut-clipboard" () } # For UTF-8 inputs ! - bind "F11" {"insert-at-cursor" ("∀")} - bind "F12" {"insert-at-cursor" ("∃")} +# bind "F11" {"insert-at-cursor" ("∀")} +# bind "F12" {"insert-at-cursor" ("∃")} } class "GtkTextView" binding "text" @@ -36,7 +36,7 @@ widget "*.*.*.*.MessageWindow" style "views" gtk-font-name = "Sans 12" style "location" { -font_name = "Monospace 10" +font_name = "Sans 10" } widget "*location*" style "location" |