Skip to content

Conversation

@Dandandan
Copy link
Contributor

@Dandandan Dandandan commented Nov 28, 2020

This fixes the CI.
Was introduced in #8688 , I guess because the CI there ran before the merge.

@github-actions
Copy link

@nevi-me
Copy link
Contributor

nevi-me commented Nov 28, 2020

Thanks Daniël, I'm looking into what we can change in our CI to avoid running out of disk space. I'll try fix that today.

Given that CI isn't cheap (as we now see from Travis), it's not always possible to rerun CI before merging PRs, to check if they break anything merged before them.

@nevi-me
Copy link
Contributor

nevi-me commented Nov 28, 2020

CI failure is not because of tests, so I'm merging this

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants