Closed sbernauer closed 1 year ago
Extracted out of #211 as we want to give the demo today
Once the review is done, comment bors r+ (or bors merge) to merge. Further information
bors r+
bors merge
It was, thx!
Pull request successfully merged into main.
Build succeeded:
Description
Extracted out of #211 as we want to give the demo today
Review Checklist
Once the review is done, comment
bors r+
(orbors merge
) to merge. Further information