summary refs log tree commit diff
path: root/.github (unfollow)
Commit message (Expand)AuthorFilesLines
2021-08-12Remove buildkite-era commentDavid Robertson1-3/+0
2021-08-12portdb also uses coverage, so provide $TOP thereDavid Robertson1-0/+2
2021-08-12Also rename in lint.shDavid Robertson1-1/+1
2021-08-11Missed another ci->.ciDavid Robertson1-9/+9