diff options
| author | Maxime Dénès | 2018-11-21 18:33:05 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-21 18:42:12 +0100 |
| commit | fe9340263be1c28fb0dc4c7312cddd72e91253c8 (patch) | |
| tree | 2748374c125599edb8ad76d5125bd23bd51055a0 /Makefile.ci | |
| parent | 452cb15fd9647dc453cc36614cc469dfa91e3080 (diff) | |
Remove pidetop from CI
pidetop relies on some rather low level API from STM, which we'd like to
change. It does not seem maintained much anymore, and still hasn't moved
to github.
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile.ci b/Makefile.ci index 88ea64974a..d0b87fc58b 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -37,7 +37,6 @@ CI_TARGETS= \ ci-math-comp \ ci-mtac2 \ ci-paramcoq \ - ci-pidetop \ ci-plugin_tutorial \ ci-quickchick \ ci-sf \ |