chiark / gitweb /
Merge branch 'texinfo' into 'master'
authorHans-Christoph Steiner <hans@guardianproject.info>
Mon, 31 Oct 2016 17:51:16 +0000 (17:51 +0000)
committerHans-Christoph Steiner <hans@guardianproject.info>
Mon, 31 Oct 2016 17:51:16 +0000 (17:51 +0000)
commitf90adcc912f82c5ab5075815e6b0419f37fbe6e7
treea269ce9dd5d7020396badb6e0dda602bad8800ca
parent559f38cd218b857164ddba835828cfd52637b4e5
parent2e96fc1cd9336bb180c655eb020040e00e22ed7a
Merge branch 'texinfo' into 'master'

CI: use new docker image with texinfo

docs/gendocs.sh uses makeinfo.

See merge request !179