Eventually remembered to document this...
Checking pipeline status.
Merge details
mentioned in commit aa700d85
merged