sorry to do this twice - just noticed the page was a bit mixed up
Merge details
Pipeline #927 passed
Pipeline passed for c63e4de6 on master 7 years ago
merged
mentioned in commit c63e4de6
You can go ahead and push right to the repo -- no need for merge requests. Looks like you're a master of this project, so you should be able to...
(May 18, 2025 7:33pm UTC) 