[travis] Move ci files from `tools` to `dev`.

16 files changed, 3 insertions, 3 deletions

diff --git a/Makefile.ci b/Makefile.ci
index d10ff3ad96..d69028ce13 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -6,5 +6,5 @@ CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt	\
 
 # Generic rule, we use make to easy travis integraton with mixed rules
 $(CI_TARGETS): ci-%:
-	./tools/ci/ci-$*.sh
+	./dev/ci/ci-$*.sh
 
diff --git a/README.ci b/README.ci
index ed2ba9126e..dcf93cf00e 100644
--- a/README.ci
+++ b/README.ci
@@ -40,7 +40,7 @@ Maintaining your contribution manually [current method]
 ======================================
 
 To add your contribution to the Coq Travis CI set, add a script for
-building your library to `tools/ci/`, update `.travis.yml` and
+building your library to `dev/ci/`, update `.travis.yml` and
 `Makefile.ci`. Then, submit a PR.
 
 Maintaining your contribution as an OPAM package [work in progress] [to be implemented]
@@ -67,7 +67,7 @@ repositories of some of the tests so they can provide fixed
 developments.
 
 The general idea is that the PR author will drop a file
-`tools/ci/overlays/$branch.overlay` where branch name is taken from
+`dev/ci/overlays/$branch.overlay` where branch name is taken from
 `${TRAVIS_PULL_REQUEST_BRANCH:-$TRAVIS_BRANCH}`
 that is to say, the name of the original branch for the PR.
 
diff --git a/tools/ci/ci-color.sh b/dev/ci/ci-color.sh
index 78ae7f02f9..78ae7f02f9 100755
--- a/tools/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
diff --git a/tools/ci/ci-common.sh b/dev/ci/ci-common.sh
index 2a6601e045..2a6601e045 100644
--- a/tools/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
diff --git a/tools/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index d4023c9165..d4023c9165 100755
--- a/tools/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
diff --git a/tools/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 4a23e51be6..4a23e51be6 100755
--- a/tools/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
diff --git a/tools/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
index 18d7561804..18d7561804 100755
--- a/tools/ci/ci-cpdt.sh
+++ b/dev/ci/ci-cpdt.sh
diff --git a/tools/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index c594f83603..c594f83603 100755
--- a/tools/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
diff --git a/tools/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index b9cf649a1a..b9cf649a1a 100755
--- a/tools/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
diff --git a/tools/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 8f82ba9f21..8f82ba9f21 100755
--- a/tools/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
diff --git a/tools/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index c1306e070d..c1306e070d 100755
--- a/tools/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
diff --git a/tools/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 9127c18951..9127c18951 100755
--- a/tools/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
diff --git a/tools/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index b833792419..b833792419 100755
--- a/tools/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
diff --git a/tools/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index 9a9bd3648b..9a9bd3648b 100755
--- a/tools/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
diff --git a/tools/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 5e41211f1a..5e41211f1a 100755
--- a/tools/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
diff --git a/tools/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
index 2161a11461..2161a11461 100755
--- a/tools/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh