Merge branch 'master' of https://git.gnunet.org/gnunet
authorlurchi <lurchi@strangeplace.net>
Wed, 26 Jun 2019 18:04:52 +0000 (20:04 +0200)
committerlurchi <lurchi@strangeplace.net>
Wed, 26 Jun 2019 18:04:56 +0000 (20:04 +0200)

Trivial merge