Add pull_request event to github actions hooks

[k-nasa]

#253

I forgot to add pull_request event hooks.
Probably necessary, but what about?

[k-nasa]

GitHub actions worked. Would have been necessary

[k-nasa]

Ok. I fixed.
However, is ci not working when pushed to master branch?

[yoshuawuyts]

However, is ci not working when pushed to master branch?

Not sure; in general all of our commits are through PRs anyway, and if Bors works then we don't need to run the extra CI run on master merges.

It looks like Clippy is failing though; not sure what's going on as it's a lot of JSON output.

edit: ah I just saw #270

[k-nasa]

@yoshuawuyts My imagination is that this access token is mine (the person who pushed it) and I don't have write access, so it may have failed.

token: ${{ secrets.GITHUB_TOKEN }}

[yoshuawuyts]

Alright then; let's merge this and see if it works 🤞