Fix merge from develop to master.

This commit is contained in:
JF 2020-09-27 13:18:54 +02:00
commit 92d9c58a92