summaryrefslogtreecommitdiff
path: root/ide/coqide-gtk2rc
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide-gtk2rc')
-rw-r--r--ide/coqide-gtk2rc39
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"