Closed marcobonici closed 2 years ago
I've modified the CI workflow in bbb5de6, per the GitHub documentation. It should now trigger if we get a pull request. Of course, we won't know for sure until someone submits another pull request :shrug:
Thank you, @lonbar ! I'll close the Issue.
Actually the CI is triggered only when we push a commit. However, we it should be possible to trigger the CI also when there is a PR. For instance, someone forked our repo and made a PR, which did not trigger the CI. What do you think @lonbar @nikosarcevic ?