diff options
author | David Allsopp <david.allsopp@metastack.com> | 2021-02-09 12:23:53 +0000 |
---|---|---|
committer | David Allsopp <david.allsopp@metastack.com> | 2021-02-09 12:23:53 +0000 |
commit | 62386282a34d89a5f6121fe2df5ba819abaef7a0 (patch) | |
tree | 2399e6759b8770d6c8db306091c3f8a6577f9a06 /.github/workflows | |
parent | 1ae9aff6918ae0ecf8585792506fa0cf4f270700 (diff) | |
download | ocaml-62386282a34d89a5f6121fe2df5ba819abaef7a0.tar.gz |
Move Travis Changes and check-typo checks to GHA
Diffstat (limited to '.github/workflows')
-rw-r--r-- | .github/workflows/hygiene.yml | 70 |
1 files changed, 70 insertions, 0 deletions
diff --git a/.github/workflows/hygiene.yml b/.github/workflows/hygiene.yml new file mode 100644 index 0000000000..9fa46daef7 --- /dev/null +++ b/.github/workflows/hygiene.yml @@ -0,0 +1,70 @@ +name: Hygiene +on: + push: + pull_request: + types: [opened, synchronize, reopened, labeled, unlabeled] + +jobs: + hygiene: + name: Checks + runs-on: ubuntu-latest + steps: + - name: GitHub Context + run: echo $GITHUB_CONTEXT + env: + GITHUB_CONTEXT: ${{ toJson(github) }} + # Comment out the line below to enable (debugging) display of the github + # context variable. + if: failure() + + - uses: actions/checkout@v2 + with: + fetch-depth: 50 + + - name: Changes updated + run: >- + tools/ci/actions/check-changes-modified.sh + 'pull_request' + '${{ github.event.pull_request.base.ref }}' + '${{ github.event.pull_request.base.sha }}' + '${{ github.event.pull_request.head.ref }}' + '${{ github.event.pull_request.head.sha }}' + if: >- + !contains(github.event.pull_request.labels.*.name, 'no-change-entry-needed') + && github.event_name == 'pull_request' + + - name: configure correctly generated + run: >- + tools/ci/actions/check-configure.sh + '${{ github.event_name }}' + '${{ github.event.pull_request.base.ref }}' + '${{ github.event.pull_request.base.sha }}' + '${{ github.event.pull_request.head.ref }}' + '${{ github.event.pull_request.head.sha }}' + '${{ github.event.ref }}' + '${{ github.event.before }}' + '${{ github.event.ref }}' + '${{ github.event.after }}' + if: ${{ always() }} + + - name: check-typo revered + run: >- + tools/ci/actions/check-typo.sh + '${{ github.event_name }}' + '${{ github.event.pull_request.base.ref }}' + '${{ github.event.pull_request.base.sha }}' + '${{ github.event.pull_request.head.ref }}' + '${{ github.event.pull_request.head.sha }}' + '${{ github.event.ref }}' + '${{ github.event.before }}' + '${{ github.event.ref }}' + '${{ github.event.after }}' + if: ${{ always() }} + + - name: check-typo on whole tree + run: tools/check-typo + if: >- + github.event_name == 'push' + && (startsWith(github.event.ref, 'refs/heads/4.') + || github.event.ref == 'refs/heads/trunk') + && always() |