File tree Expand file tree Collapse file tree 1 file changed +42
-0
lines changed
Expand file tree Collapse file tree 1 file changed +42
-0
lines changed Original file line number Diff line number Diff line change 1+ name : Check Generated Files
2+
3+ on :
4+ pull_request : {}
5+ push :
6+ branches :
7+ - main
8+
9+ concurrency :
10+ group : ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
11+ cancel-in-progress : true
12+
13+ jobs :
14+ check-generated :
15+ runs-on : ubuntu-latest
16+ container : returntocorp/ocaml:alpine
17+ steps :
18+ - name : Checkout tree
19+ uses : actions/checkout@v4
20+
21+ - name : Setup
22+ shell : bash
23+ run : |
24+ git config --global --add safe.directory "$(pwd)"
25+ eval $(HOME=/root opam env)
26+ apk add py3-pip
27+ pip install check-jsonschema mypy --break-system-packages
28+ make setup
29+
30+ - name : Regenerate files
31+ shell : bash
32+ run : |
33+ eval $(HOME=/root opam env)
34+ make
35+
36+ - name : Check for changes
37+ run : |
38+ git diff --exit-code || {
39+ echo "::error::Generated files are out of date. Please run 'make setup && make' and commit the changes."
40+ git diff --stat
41+ exit 1
42+ }
You can’t perform that action at this time.
0 commit comments