chiark / gitweb /
Merge branch 'master' into 'master'
authorHans-Christoph Steiner <hans@guardianproject.info>
Thu, 3 May 2018 12:11:48 +0000 (12:11 +0000)
committerHans-Christoph Steiner <hans@guardianproject.info>
Thu, 3 May 2018 12:11:48 +0000 (12:11 +0000)
Three random fixes

See merge request fdroid/fdroidserver!496


Trivial merge