Merge branch 'master' into debian

This commit is contained in:
Benoît S. 2018-04-10 15:46:34 +02:00
commit 1e39fd9d12