src/ide/why3ide.ml · 30f8256aa9964b1a44797596b048e36f5cee4cdb · Why3 / why3 · GitLab

Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Find file Blame History Permalink

IDE: fix use select_iter instead of selection#select_iter · 30f8256a

Sylvain Dailler authored Jun 28, 2018

select_iter changes the cursor used by the goals_view for changing nodes
with keyboard arrow keys. selection#select_iter should be avoided alone.

30f8256a

why3ide.ml 82.7 KB