aboutsummaryrefslogtreecommitdiff
path: root/.github
AgeCommit message (Collapse)Author
2022-02-09github: Remove GitHub actions.Arun Isaac
We have our own laminar CI and no longer need GitHub actions. * .github/workflows: Delete directory.
2021-12-10Remove pull request template.Arun Isaac
People are not using the pull request template properly. Often, the fields remain unfilled, and the placeholders are not deleted. This is cognitively taxing for reviewers. Also, most of our changes are better described in the commit log than in the pull request description. And, our reviews are quite cursory and don't need a detailed pull request description for the reviewer to act on. * .github/PULL_REQUEST_TEMPLATE.md: Delete file.
2021-11-11Update PULL_REQUEST_TEMPLATE.md.Arun Isaac
2021-05-08Add issue and PR templatesBonfaceKilz
2021-02-24Add type checking to gh workflowsBonfaceKilz
2021-02-12Create python-app.ymlBonfaceKilz