Closed cchwala closed 4 months ago
Some problem from #5 seems to have resulted in CI not running for new commits in PRs. Here I try to fix that...
not sure if the problem was with Github that its CI just did not run correctly, or my very minor change here solved the problem. I think the former is more likely. Anyway, looks like CI is working now.
Some problem from #5 seems to have resulted in CI not running for new commits in PRs. Here I try to fix that...