Merge branch 'patch-1' into 'master'
Dedication to E. Pipping
See merge request !427 (merged)
(cherry picked from commit f0d33bc3)
b44118cc Dedication to E. Pipping
Dedication to E. Pipping
See merge request !427 (merged)
(cherry picked from commit f0d33bc3)
b44118cc Dedication to E. Pipping
enabled an automatic merge when the pipeline for 427c3261 succeeds
merged
mentioned in commit 7196b9e5