diff options
Diffstat (limited to '.github/workflows')
| -rw-r--r-- | .github/workflows/main.yml | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml new file mode 100644 index 0000000000..2b1a968c28 --- /dev/null +++ b/.github/workflows/main.yml @@ -0,0 +1,31 @@ +name: main + +on: [push, pull_request] + +jobs: + build: + name: ${{ matrix.name }} + runs-on: ${{ matrix.os }} + strategy: + matrix: + include: + - name: linux-debug + os: ubuntu-latest + env: OCAMLRUNPARAM=v=0,V=1 USE_RUNTIME=d + - name: linux + os: ubuntu-latest + - name: macos + os: macos-latest + + steps: + - name: Checkout + uses: actions/checkout@v2 + - name: configure tree + run: | + MAKE_ARG=-j XARCH=x64 bash -xe tools/ci/actions/runner.sh configure + - name: Build + run: | + MAKE_ARG=-j bash -xe tools/ci/actions/runner.sh build + - name: Run the testsuite + run: | + ${{ matrix.env }} bash -xe tools/ci/actions/runner.sh test |