aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide_main.ml4
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-27 15:31:30 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-27 15:31:30 +0000
commitbbf334b38ae4c57b4d619a8f98acc488077efca4 (patch)
tree91b013df3287c9a806971c1b8c47c5c519125a0f /ide/coqide_main.ml4
parent9af3413edd3c82e99766bb3c2541d1cf8920c006 (diff)
Removed the quasi-useless gtk2rc file and the documentation that went with it. Now CoqIDE is not anymore totally irrespectful of the local configuration of themes, in particular w.r.t. to menu fonts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15251 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide_main.ml4')
-rw-r--r--ide/coqide_main.ml48
1 files changed, 1 insertions, 7 deletions
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index db2b2361c..1e71b8da4 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -67,13 +67,7 @@ END
let () =
Coqide.ignore_break ();
ignore (GtkMain.Main.init ());
- initmac () ;
- (try
- let gtkrcdir = List.find
- (fun x -> Sys.file_exists (Filename.concat x "coqide-gtk2rc"))
- Minilib.xdg_config_dirs in
- GtkMain.Rc.add_default_file (Filename.concat gtkrcdir "coqide-gtk2rc");
- with Not_found -> ());
+ initmac ();
(* Statup preferences *)
begin
try Preferences.load_pref ()