Merge pull request #12783 from keszybz/a-few-unrelated-fixes
authorFrantisek Sumsal <frantisek@sumsal.cz>
Wed, 12 Jun 2019 17:52:48 +0000 (17:52 +0000)
committerGitHub <noreply@github.com>
Wed, 12 Jun 2019 17:52:48 +0000 (17:52 +0000)
A few unrelated fixes


Trivial merge