diff options
| author | Emilio Jesus Gallego Arias | 2017-02-04 23:55:24 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-02-07 10:27:17 +0100 |
| commit | 138a4da7f0133d7b4ea06cfbc938d23ddb88c97d (patch) | |
| tree | 8f54418ccec857d9d5dea108ccaed0cf8de221de /tools | |
| parent | 3a66f149a34613ef0ed04046fed3947e8e720cd6 (diff) | |
[travis] [External CI] Script renaming.
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 |