diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
| commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
| tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /ide/coqide-gtk2rc | |
| parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) | |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'ide/coqide-gtk2rc')
| -rw-r--r-- | ide/coqide-gtk2rc | 39 |
1 files changed, 0 insertions, 39 deletions
diff --git a/ide/coqide-gtk2rc b/ide/coqide-gtk2rc deleted file mode 100644 index 9da99551..00000000 --- a/ide/coqide-gtk2rc +++ /dev/null @@ -1,39 +0,0 @@ -# Some default functions for CoqIde. You may copy the file in $XDG_CONFIG_HOME -# ($HOME/.config/coq/) and edit as you want. See -# http://developer.gnome.org/doc/API/2.0/gtk/gtk-Resource-Files.html -# 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" - -#pixmap_path "/home/" - -binding "text" { - bind "<ctrl>k" { "set-anchor" () - "move-cursor" (display-line-ends,1,0) - "move-cursor" (visual-positions,1,0) - "cut-clipboard" () - } - bind "<ctrl>w" { "cut-clipboard" () } - -# For UTF-8 inputs ! -# bind "F11" {"insert-at-cursor" ("∀")} -# bind "F12" {"insert-at-cursor" ("∃")} -} -class "GtkTextView" binding "text" - - -gtk-font-name = "Sans 12" - -style "location" { -font_name = "Sans 10" -} -widget "*location*" style "location" - - -gtk-can-change-accels = 1 - -style "men" { -# -} -widget "GtkMenu" style "men" |