Merge branch 'master' into issue_1453
authorKim Kulling <kimkulling@users.noreply.github.com>
Tue, 10 Oct 2017 16:20:22 +0000 (18:20 +0200)
committerGitHub <noreply@github.com>
Tue, 10 Oct 2017 16:20:22 +0000 (18:20 +0200)

Trivial merge