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