This repository was archived by the owner on May 23, 2023. It is now read-only.

Description
Right now, develop builds look dire. In order to get a green light again, I think (at least) the following steps need to be done:
Q: is there a nicer way?
git checkout develop
git checkout origin/fix-develop .
git checkout develop
git commit # ae2498ac7f907dddc819185c013e9931228704d3
git merge origin/fix-develop # 025d43b7377a781be2e6d6c0ead5a7fb59bb6135
^--- thanks @ulope !
Please everyone involved in above PRs organize through this issue, so we have a happy travis guy and a ✅ again soon!