Remove CI scrippts from tools

Now that the CI scripts have been moved also on the 4.07 branch and that the
Jenkins jobs have been updated to call the scripts from their new locations,
get rid of the legacy ones.
master
Sébastien Hinderer 2018-06-05 16:42:14 +02:00
parent f572baccd5
commit 69944e9e73
2 changed files with 0 additions and 10 deletions

View File

@ -1,5 +0,0 @@
#!/bin/sh
# This is expected to be run from the toplevel of the OCaml source tree
# This script can be removed once none of the branch tested on Inria's CI
# expects to find it here, i.e. once we stop working on the 4.07 branch
./tools/ci/inria/main "$@"

View File

@ -1,5 +0,0 @@
#!/bin/sh
# This is expected to be run from the toplevel of the OCaml source tree
# This script can be removed once none of the branch tested on Inria's CI
# expects to find it here, i.e. once we stop working on the 4.07 branch
./tools/ci/inria/other-configs "$@"