diff options
| author | Hendrik Tews | 2020-12-09 20:33:57 +0100 |
|---|---|---|
| committer | hendriktews | 2020-12-19 16:43:49 +0100 |
| commit | 8bca3fbcf3e2aa51e1035ec0349dc52b652bb9ad (patch) | |
| tree | f7b7d57d77c8e55b635f8809071fe468da0b39df /ci | |
| parent | ff230ff05620b67b4493354a829923c3efe4dc8b (diff) | |
enable coq background compilation tests in github CI
extend the github workflow to additionally run the tests in
ci/compile-tests
Diffstat (limited to 'ci')
0 files changed, 0 insertions, 0 deletions