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)
commit6ae5ca6672f3c6ab891679f85fd1c791ea3aec4d
tree9aec8442720a39d4ab945b5022b85ea5faad79ba
parentee3e99a0d8a75edc90a1a4e9fb1c593a99a02bb9
parentb8eb2486b15d564e73ef9307e175ac24a186acd2
Merge pull request #118