Closed greschd closed 4 years ago
Thanks! Feel free to merge once tests pass
@giovannipizzi I think we should migrate CI to travis-ci.com (from travis-ci.org), the latter is apparently being sunset. I "requested" access for that, but can't set the permissions for that on Github myself.
Eventually I guess we want to migrate to Github Actions, but the .org -> .com migration is only a few clicks and immediately brings build times back to normal (at least, until we've run out of minutes).
Yes, I had done it in the meantime. And yes, I suggest to move to Actions as soon as someone has an hour to spend on it :-)
Failing tests fixed in #106.