diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-04 23:55:24 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-07 10:27:17 +0100 |
| commit | 138a4da7f0133d7b4ea06cfbc938d23ddb88c97d (patch) | |
| tree | 8f54418ccec857d9d5dea108ccaed0cf8de221de | |
| parent | 3a66f149a34613ef0ed04046fed3947e8e720cd6 (diff) | |
[travis] [External CI] Script renaming.
| -rw-r--r-- | .travis.yml | 6 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | Makefile.ci | 13 | ||||
| -rw-r--r-- | Makefile.contrib | 13 | ||||
| -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 |
7 files changed, 18 insertions, 18 deletions
diff --git a/.travis.yml b/.travis.yml index 14573e295..c85122ac9 100644 --- a/.travis.yml +++ b/.travis.yml @@ -21,9 +21,9 @@ env: # Main test suites matrix: - TEST_TARGET="validate" TW="travis_wait" - - TEST_TARGET="contrib-hott" - - TEST_TARGET="contrib-math-comp" - - TEST_TARGET="contrib-compcert" + - TEST_TARGET="ci-hott" + - TEST_TARGET="ci-math-comp" + - TEST_TARGET="ci-compcert" matrix: @@ -246,9 +246,9 @@ devdocclean: rm -f $(OCAMLDOCDIR)/html/*.html ########################################################################### -# Contrib tests +# Continuous Intregration Tests ########################################################################### -include Makefile.contrib +include Makefile.ci ########################################################################### # Emacs tags diff --git a/Makefile.ci b/Makefile.ci new file mode 100644 index 000000000..ada698e0a --- /dev/null +++ b/Makefile.ci @@ -0,0 +1,13 @@ +.PHONY: ci-all ci-hott ci-math-comp ci-compcert + +ci-all: ci-hott ci-math-comp ci-compcert + +# TODO Do generic rule +ci-hott: + ./tools/ci/ci-hott.sh + +ci-math-comp: + ./tools/ci/ci-math-comp.sh + +ci-compcert: + ./tools/ci/ci-compcert.sh diff --git a/Makefile.contrib b/Makefile.contrib deleted file mode 100644 index 2e3ed94c5..000000000 --- a/Makefile.contrib +++ /dev/null @@ -1,13 +0,0 @@ -.PHONY: contrib-all contrib-hott contrib-math-comp - -contrib-all: contrib-hott contrib-math-comp - -# TODO Do generic rule -contrib-hott: - ./tools/ci/contrib-hott.sh - -contrib-math-comp: - ./tools/ci/contrib-math-comp.sh - -contrib-compcert: - ./tools/ci/contrib-compcert.sh diff --git a/tools/ci/contrib-compcert.sh b/tools/ci/ci-compcert.sh index 416e28325..416e28325 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 35af76ceb..35af76ceb 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 39a92a2d8..39a92a2d8 100755 --- a/tools/ci/contrib-math-comp.sh +++ b/tools/ci/ci-math-comp.sh |