This reverts merge request !1830 (merged)
Checking pipeline status.
Pipeline #5898157 passed
Pipeline passed for 5595699a on RD_2018-patches 1 year ago
assigned to @ngrieser
mentioned in commit 5595699a
merged