Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
stdpp
Merge requests
!142
Merged
Created
Apr 09, 2020
by
Michael Sammler
@msammler
Owner
2 of 2 tasks completed
2/2 tasks
Options
Added select and select_revert tactics
Overview
48
Commits
1
Changes
2
As discussed with
@robbertkrebbers
open points:
Names of the tactics (What are the names in Mtac?
@janno
)
Changelog entry?
Edited
Apr 10, 2020
by
Michael Sammler