Commit 81bbad2b authored by MARCHE Claude's avatar MARCHE Claude

IDE GTK: show the tools menu on right click

parent 0c327fa2
......@@ -1250,6 +1250,8 @@ let (_ : GtkSignal.id) =
| [r] -> on_selected_row r;
if !has_right_click then
(* TODO here show the menu *)
tools_menu#popup ~button:1 ~time:0l;
(*
GToolbox.popup_menu ~entries:[
`I("Mark Obsolete",
(* TODO add a mark_obsolete function *)
......@@ -1266,6 +1268,7 @@ let (_ : GtkSignal.id) =
`I("Choix 2.3",(fun () -> Format.eprintf "Popup menu: choix 2.3 active@."));
]
~button:1 ~time:0l;
*)
has_right_click := false
| _ -> ()
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment