aboutsummaryrefslogtreecommitdiff
path: root/.github
AgeCommit message (Expand)Author
2022-02-09github: Remove GitHub actions....We have our own laminar CI and no longer need GitHub actions. * .github/workflows: Delete directory. Arun Isaac
2021-12-10Remove pull request template....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. Arun Isaac
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