Merge this repo with TuringLang/.github?

[yebai]

@penelopeysm @shravanngoswamii Thanks for the nice work. Is it possible to merge this repo into https://github.com/TuringLang/.github?

[penelopeysm]

My understanding is that they're different things; the .github repo contains templates to help set up workflows in other repos (workflows = .yml files), whereas these are just individual steps which can be used within those workflows. The former makes it easier to construct standardised workflows, but doesn't lead to any code sharing in the way this does.

I suppose that in principle we could keep actions inside the .github repo as well, but I do like having the descriptive repo name.

[yebai]

How about storing them in TuringLang/.github/actions folder?

@devmotion, is there any good practice for this?