aboutsummaryrefslogtreecommitdiffstats
path: root/.github
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-11-14 19:21:00 +0000
committerYann Herklotz <git@yannherklotz.com>2020-11-14 19:21:00 +0000
commit8d846f39e7273981bbd0c6c38e91a7bafeff08cb (patch)
tree161957893dac48a7a1400106e2435c76e180712d /.github
parent9fb5632f42e58e5e53bed34e22a656ba04f3fe74 (diff)
downloadvericert-8d846f39e7273981bbd0c6c38e91a7bafeff08cb.tar.gz
vericert-8d846f39e7273981bbd0c6c38e91a7bafeff08cb.zip
Add more tracking files to github workflow
Diffstat (limited to '.github')
-rw-r--r--.github/workflows/main.yml6
1 files changed, 6 insertions, 0 deletions
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 5b4899c..c0e9606 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -7,12 +7,18 @@ on:
- "**.v"
- "**.ml"
- "**.mli"
+ - "**.yml"
+ - "*.nix"
+ - Makefile
pull_request:
branches: [ master ]
paths:
- "**.v"
- "**.ml"
- "**.mli"
+ - "**.yml"
+ - "*.nix"
+ - Makefile
workflow_dispatch: {}
jobs: