summaryrefslogtreecommitdiff
path: root/.github/workflows
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2021-02-09 12:23:53 +0000
committerDavid Allsopp <david.allsopp@metastack.com>2021-02-09 12:23:53 +0000
commit62386282a34d89a5f6121fe2df5ba819abaef7a0 (patch)
tree2399e6759b8770d6c8db306091c3f8a6577f9a06 /.github/workflows
parent1ae9aff6918ae0ecf8585792506fa0cf4f270700 (diff)
downloadocaml-62386282a34d89a5f6121fe2df5ba819abaef7a0.tar.gz
Move Travis Changes and check-typo checks to GHA
Diffstat (limited to '.github/workflows')
-rw-r--r--.github/workflows/hygiene.yml70
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()