chiark / gitweb /
Merge branch 'master' into 'master'
authorHans-Christoph Steiner <hans@guardianproject.info>
Fri, 22 Jan 2016 10:27:54 +0000 (10:27 +0000)
committerHans-Christoph Steiner <hans@guardianproject.info>
Fri, 22 Jan 2016 10:27:54 +0000 (10:27 +0000)
commit16c220517d4d105c4b2f24e23b0ffcaa9fd14fee
tree8f3c5e0f06d65d36c892eb644b976d0fec9a8d06
parent0003e4c742cf400e18f1f20bc0ae3602dce95237
parenta2b20f4c8477b1dfbd48514e2020be38e886b186
Merge branch 'master' into 'master'

Reproducibly build documentation

The two commits fix reproducibility problems detected by the Debian CI:

https://reproducible.debian.net/rb-pkg/unstable/amd64/fdroidserver.html

See merge request !84