diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-25 10:25:15 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-25 10:25:15 +0000 |
| commit | 3d15fc36309eb9bd6bef72ebac260b78b11e23f3 (patch) | |
| tree | 75deaa023767d350dc575abdfd2a417cd80886fb /ide/preferences.ml | |
| parent | f3d29cafda385f23e191f210565d2798467be0e3 (diff) | |
Icons in CoqIdE preference panel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14590 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/preferences.ml')
| -rw-r--r-- | ide/preferences.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 8d7723bb0..3f2c69acd 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -586,30 +586,30 @@ let configure ?(apply=(fun () -> ())) () = (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!! (shame on Benjamin) *) let cmds = - [Section("Fonts", + [Section("Fonts", Some `SELECT_FONT, [config_font]); - Section("Files", + Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) encodings; ]); - Section("Project", + Section("Project", Some (`STOCK "gtk-page-setup"), [project_file_name;read_project; ]); (* Section("Appearance", config_appearance); *) - Section("Externals", + Section("Externals", None, [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print; cmd_editor; cmd_browse;doc_url;library_url]); - Section("Tactics Wizard", + Section("Tactics Wizard", None, [automatic_tactics]); - Section("Shortcuts", + Section("Shortcuts", Some `PREFERENCES, [modifiers_valid; modifier_for_tactics; modifier_for_templates; modifier_for_display; modifier_for_navigation]); - Section("Misc", + Section("Misc", Some `ADD, misc)] in (* |