Merge origin/ci into ci

This commit is contained in:
paolo
2016-04-11 10:02:16 +02:00