aboutsummaryrefslogtreecommitdiff
path: root/.github
diff options
context:
space:
mode:
authorErik Martin-Dorel2020-05-04 22:02:42 +0200
committerGitHub2020-05-04 22:02:42 +0200
commit24e1c5ae3dec16c972babcf44786eb7eff3c6b53 (patch)
tree03e9d25be79e97fbc6b9ba42cdae2e892617522b /.github
parent23db83dc4141d89530f6381ba49f56399682d4e0 (diff)
parent63dc6a6bc23f2eff3e3c3bbee9e79d4097d8f139 (diff)
Merge pull request #486 from ProofGeneral/coq-tests-for-master
Coq tests for master
Diffstat (limited to '.github')
-rw-r--r--.github/ert.json14
-rw-r--r--.github/workflows/test.yml11
2 files changed, 23 insertions, 2 deletions
diff --git a/.github/ert.json b/.github/ert.json
new file mode 100644
index 00000000..02dc5548
--- /dev/null
+++ b/.github/ert.json
@@ -0,0 +1,14 @@
+{
+ "problemMatcher": [
+ {
+ "owner": "ert-problem-matcher",
+ "severity": "error",
+ "pattern": [
+ {
+ "regexp": "^\\s+((?:FAILED|failed|SKIPPED|skipped|ABORTED|aborted|QUIT|quit)\\s+[0-9]+/[0-9]+\\s+.*)$",
+ "message": 1
+ }
+ ]
+ }
+ ]
+}
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 984f0cc5..db4bb766 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -3,8 +3,9 @@ name: CI
on:
push:
branches:
- - master
- - hybrid
+ #- master
+ #- hybrid
+ - "**"
pull_request:
branches:
- '**'
@@ -66,6 +67,9 @@ jobs:
steps:
- uses: actions/checkout@v2
+ - name: Add ert problem matcher
+ run: echo "::add-matcher::.github/ert.json"
+
- uses: coq-community/docker-coq-action@v1
id: docker-coq-action
with:
@@ -81,5 +85,8 @@ jobs:
sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends emacs
endGroup
startGroup Run tests
+ sudo chown -R coq:coq ./ci
./ci/test.sh
endGroup
+
+ # - run: echo "::remove-matcher owner=ert-problem-matcher::"