aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-basic-overlay.sh
diff options
context:
space:
mode:
authorEnrico Tassi2020-09-11 16:37:42 +0200
committerEnrico Tassi2020-09-11 16:37:42 +0200
commitf6ab4e9520c6dd2de6d6247347ca005c3fe4213c (patch)
tree5253e30cc856875969be4bfe53811657f9c9f8e8 /dev/ci/ci-basic-overlay.sh
parente1a8da8b83aa3ae96ac05c2bc6606aa0719aa64f (diff)
[ci] [mathcomp] run the test suite
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions