diff options
| author | pboutill | 2011-11-20 20:03:03 +0000 |
|---|---|---|
| committer | pboutill | 2011-11-20 20:03:03 +0000 |
| commit | ab6f28a2a5251cc7ef18948dc619781e82e43e71 (patch) | |
| tree | ccbb1a858741c94bf388bef61a22e969c5fb6561 /ide | |
| parent | 6600b4e71cc82fc2a7c00e8dc1d4aa5ec1787cf7 (diff) | |
coqide-gtk2rc not dotted
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14695 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide-gtk2rc (renamed from ide/.coqide-gtk2rc) | 4 | ||||
| -rw-r--r-- | ide/coqide_main.ml4 | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/ide/.coqide-gtk2rc b/ide/coqide-gtk2rc index 11c53dad29..621d4e8479 100644 --- a/ide/.coqide-gtk2rc +++ b/ide/coqide-gtk2rc @@ -1,5 +1,5 @@ -# Some default functions for CoqIde. You may copy the file in your HOME and -# edit as you want. See +# 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. diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index f09ef2492a..36257e8db1 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -73,9 +73,9 @@ let () = Minilib.coqlib := Coq.check_coqlib args; Coqide.sup_args := args; Coqide.ignore_break (); - GtkMain.Rc.add_default_file (Ideutils.lib_ide_file ".coqide-gtk2rc"); + GtkMain.Rc.add_default_file (Ideutils.lib_ide_file "coqide-gtk2rc"); (try - GtkMain.Rc.add_default_file (Filename.concat Minilib.home ".coqide-gtk2rc"); + GtkMain.Rc.add_default_file (Filename.concat Minilib.xdg_config_home "coqide-gtk2rc"); with Not_found -> ()); ignore (GtkMain.Main.init ()); initmac () ; |