Minor, but since I spotted it, might as well fix
Merge details
Pipeline #2020 passed
Pipeline passed for 628a2ae7 on master 5 years ago
merged
mentioned in commit 628a2ae7