diff options
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/ci-compcert.sh (renamed from tools/ci/contrib-compcert.sh) | 0 | ||||
| -rwxr-xr-x | tools/ci/ci-hott.sh (renamed from tools/ci/contrib-hott.sh) | 0 | ||||
| -rwxr-xr-x | tools/ci/ci-math-comp.sh (renamed from tools/ci/contrib-math-comp.sh) | 0 |
3 files changed, 0 insertions, 0 deletions
diff --git a/tools/ci/contrib-compcert.sh b/tools/ci/ci-compcert.sh index 416e283254..416e283254 100755 --- a/tools/ci/contrib-compcert.sh +++ b/tools/ci/ci-compcert.sh diff --git a/tools/ci/contrib-hott.sh b/tools/ci/ci-hott.sh index 35af76ceb7..35af76ceb7 100755 --- a/tools/ci/contrib-hott.sh +++ b/tools/ci/ci-hott.sh diff --git a/tools/ci/contrib-math-comp.sh b/tools/ci/ci-math-comp.sh index 39a92a2d89..39a92a2d89 100755 --- a/tools/ci/contrib-math-comp.sh +++ b/tools/ci/ci-math-comp.sh |