diff options
| author | pboutill | 2011-07-27 14:33:19 +0000 |
|---|---|---|
| committer | pboutill | 2011-07-27 14:33:19 +0000 |
| commit | 5252abc632f7b79600a34d6c0712b6d2c070ade0 (patch) | |
| tree | 42f83e5c18ab97c5800666f085e037a11c7579a0 /ide/command_windows.ml | |
| parent | 6c03e540c5e4461432c4e1937ce5cbbbb148e145 (diff) | |
Coqide: GEdit.combo is deprecated since Gtk2.4! We now use GEdit.combo_box_entry_text
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14306 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/command_windows.ml')
| -rw-r--r-- | ide/command_windows.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index e42c57abec..739435df4f 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -74,14 +74,10 @@ object(self) notebook#goto_page (notebook#page_num frame#coerce); let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in let hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in - let combo = GEdit.combo ~popdown_strings:Coq_commands.state_preserving - ~enable_arrow_keys:true - ~allow_empty:false - ~value_in_list:false (* true is not ok with disable_activate...*) + let (combo,_) = GEdit.combo_box_entry_text ~strings:Coq_commands.state_preserving ~packing:hbox#pack () in - combo#disable_activate (); let on_activate c () = if List.mem combo#entry#text Coq_commands.state_preserving then c () else prerr_endline "Not a state preserving command" |