diff options
| -rw-r--r-- | .github/workflows/main.yml | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 44309a2..7e04aa3 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -1,19 +1,5 @@ name: CI -on: - push: - branches: [ master ] - paths: - - '**.v' - - '**.ml' - - '**.mli' - pull_request: - branches: [ master ] - paths: - - '**.v' - - '**.ml' - - '**.mli' - jobs: build: runs-on: ubuntu-latest |