aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-pidetop.sh
AgeCommit message (Expand)Author
2018-06-02[ci] Expose updated `OCAMLPATH` for CI users.Emilio Jesus Gallego Arias
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-05-02[ci]: add pidetop (fix #7336)Enrico Tassi