Nous avons procédé ce jeudi matin 08 avril 2021 à une MAJ de sécurité urgente. Nous sommes passé de la version 13.9.3 à la version 13.9.5 les releases notes correspondantes sont ici:
https://about.gitlab.com/releases/2021/03/17/security-release-gitlab-13-9-4-released/
https://about.gitlab.com/releases/2021/03/31/security-release-gitlab-13-10-1-released/

Commit 35ef6310 authored by Sylvain Dailler's avatar Sylvain Dailler

Added navigation in the shell.

parent 0c6d5fea
......@@ -502,6 +502,10 @@ let commands =
"ngr", "get to the next goal right", ngr_ret_p;
"pcur", "print tree rooted at current position", (print_position_p cont.controller_session zipper);
"tf", "test a transformation having a formula as argument", test_transformation_with_term_arg;
"zu", "navigation up, parent", (fun _ _ -> ignore (zipper_up ()));
"zd", "navigation down, left child", (fun _ _ -> ignore (zipper_down ()));
"zl", "navigation left, left brother", (fun _ _ -> ignore (zipper_left ()));
"zr", "navigation right, right brother", (fun _ _ -> ignore (zipper_right ()))
]
let commands_table = Stdlib.Hstr.create 17
......
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