Merge branch 'master' into json-tool
authorWerner Koch <wk@gnupg.org>
Tue, 20 Mar 2018 10:13:14 +0000 (11:13 +0100)
committerWerner Koch <wk@gnupg.org>
Tue, 20 Mar 2018 10:13:14 +0000 (11:13 +0100)

Trivial merge