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/tools | |
| 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/tools')
0 files changed, 0 insertions, 0 deletions