github repo and gitlab repo have diverged and merging this would bring them back in sync.
enabled an automatic merge when the pipeline for 447d74e5 succeeds
Thanks!
mentioned in commit dfe5d3e4
merged
