diff options
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" |