diff options
| author | notin | 2006-09-29 12:39:24 +0000 |
|---|---|---|
| committer | notin | 2006-09-29 12:39:24 +0000 |
| commit | 8746bc44bbfa32a0d8b06eeb61f0a12765c2f747 (patch) | |
| tree | bceeb4cc4fe36ac2c4ec59b8229a55f2bc00e31a /ide/command_windows.ml | |
| parent | 296f9f8d9b92aa466d92bc970e13259ffdeaf760 (diff) | |
Suppression des warnings à la compilation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9189 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/command_windows.ml')
| -rw-r--r-- | ide/command_windows.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 78de678f5f..b696704eea 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -15,7 +15,7 @@ class command_window () = ~position:`CENTER ~title:"CoqIde queries" ~show:false () in - let accel_group = GtkData.AccelGroup.create () in + let _ = GtkData.AccelGroup.create () in let vbox = GPack.vbox ~homogeneous:false ~packing:window#add () in let toolbar = GButton.toolbar ~orientation:`HORIZONTAL @@ -52,7 +52,7 @@ class command_window () = () in - let kill_page_menu = + let _ = toolbar#insert_button ~tooltip:"Kill Page" ~text:"Kill Page" |