Merge pull request #118
authorHerbert Valerio Riedel <hvr@gnu.org>
Mon, 30 Jul 2018 21:48:50 +0000 (23:48 +0200)
committerGitHub <noreply@github.com>
Mon, 30 Jul 2018 21:48:50 +0000 (23:48 +0200)

Trivial merge