MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit 20df9505 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Ide: command-line - adding again the description of commands in the popup.

parent 9b1cf998
......@@ -1967,9 +1967,13 @@ let init_completion provers transformations strategies commands =
List.iter add_submenu_strategy strategies;
command_entry_completion#set_text_column completion_col;
(* does not work: it replaces the previous column as text result
command_entry_completion#set_text_column completion_desc;
*)
(* Adding a column which contains the description of the
prover/transformation/strategy. *)
let name_renderer = GTree.cell_renderer_text [ ] in
name_renderer#set_properties [`BACKGROUND "lightgrey"];
command_entry_completion#pack name_renderer;
command_entry_completion#add_attribute name_renderer "text" completion_desc;
command_entry_completion#set_match_func match_function;
command_entry#set_completion command_entry_completion
......
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