chiark / gitweb /
Merge branch 'ci-bump' into 'master'
authorDaniel Martí <mvdan@mvdan.cc>
Thu, 5 May 2016 11:14:27 +0000 (11:14 +0000)
committerDaniel Martí <mvdan@mvdan.cc>
Thu, 5 May 2016 11:14:27 +0000 (11:14 +0000)
commit736391d3d93428ffcf037325c47f75604b3fe9e2
treeb61a8157245a0e19466997f9468c96db69c40130
parent5117562df4e59a24c7c80429adf1f6e5c0d381aa
parent38790830f432c2492218f4e5efd497fd19cfbb97
Merge branch 'ci-bump' into 'master'

CI: Bump image

This is basically just an SDK update. We're now using the tools zip,
which is about 200MB smaller. Not entirely sure why, but things still
work.

See merge request !123