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 /dev/ci/ci-basic-overlay.sh | |
| 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 'dev/ci/ci-basic-overlay.sh')
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 4d5834eeb6..96bc5be7ff 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -215,13 +215,6 @@ : "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}" ######################################################################## -# pidetop -######################################################################## -: "${pidetop_CI_REF:=v8.9}" -: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}" -: "${pidetop_CI_ARCHIVEURL:=${pidetop_CI_GITURL}/get}" - -######################################################################## # ext-lib ######################################################################## : "${ext_lib_CI_REF:=master}" |