From fc1eee2e4d5f1602de7c175a93ff9409b609a2d9 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 14 Aug 2020 00:07:17 +0100 Subject: Remove on: --- .github/workflows/main.yml | 14 -------------- 1 file changed, 14 deletions(-) (limited to '.github/workflows') 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 -- cgit