aboutsummaryrefslogtreecommitdiffstats
path: root/.github
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-08-14 02:19:15 +0100
committerYann Herklotz <git@yannherklotz.com>2020-08-14 02:19:15 +0100
commit9d6979baa0e4b505862bcedee1dfd075f36579c3 (patch)
tree4e678199d57e4d87d38ad92a6ceada28e2578b2a /.github
parent6ba64984bb534d7f12433ad5370a4ea87e0341c9 (diff)
downloadvericert-9d6979baa0e4b505862bcedee1dfd075f36579c3.tar.gz
vericert-9d6979baa0e4b505862bcedee1dfd075f36579c3.zip
Fix links in gh-pages sitev1.0.1
Diffstat (limited to '.github')
-rw-r--r--.github/workflows/main.yml14
1 files changed, 14 insertions, 0 deletions
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 7e04aa3..2326979 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -1,5 +1,19 @@
name: CI
+on:
+ push:
+ branches: [ master ]
+ paths:
+ - "**.v"
+ - "**.ml"
+ - "**.mli"
+ pull_request:
+ branches: [ master ]
+ paths:
+ - "**.v"
+ - "**.ml"
+ - "**.mli"
+
jobs:
build:
runs-on: ubuntu-latest