diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-26 12:51:27 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-26 12:51:27 +0100 |
commit | b9f72bf53c831bd93d28760eefdab9ad8ffdac03 (patch) | |
tree | d4f17154717e2d0dbaa705d29808706b1ed79389 | |
parent | dea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff) |
Delete old overlays (leaving example)
8 files changed, 0 insertions, 36 deletions
diff --git a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh b/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh deleted file mode 100644 index 5c4dd1324..000000000 --- a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "1033" ] || [ "$TRAVIS_BRANCH" = "restrict-harder" ]; then - formal_topology_CI_BRANCH=ci - formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology.git - - HoTT_CI_BRANCH=coq-pr-1033 - HoTT_CI_GITURL=https://github.com/SkySkimmer/HoTT.git - - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh deleted file mode 100644 index cdca8e525..000000000 --- a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6158" ] || [ "$TRAVIS_BRANCH" = "master+some-fix-ltac-printing+refined-printers" ]; then - ltac2_CI_BRANCH=master+fix-pr6158-ltac-value-printer - ltac2_CI_GITURL=https://github.com/herbelin/ltac2.git -fi diff --git a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh b/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh deleted file mode 100644 index 6741cf26f..000000000 --- a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6169" ] || [ "$TRAVIS_BRANCH" = "clean-up/deprecated-options" ]; then - ltac2_CI_BRANCH=master - ltac2_CI_GITURL=https://github.com/Zimmi48/ltac2 -fi diff --git a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh deleted file mode 100644 index c9f1272be..000000000 --- a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6197" ] || [ "$TRAVIS_BRANCH" = "plugins+remove_locality_hack" ]; then - ltac2_CI_BRANCH=localityfixyou - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2.git -fi diff --git a/dev/ci/user-overlays/06217-coqdep-at-once.sh b/dev/ci/user-overlays/06217-coqdep-at-once.sh deleted file mode 100644 index 68e1901f7..000000000 --- a/dev/ci/user-overlays/06217-coqdep-at-once.sh +++ /dev/null @@ -1,3 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6217" ] || [ "$TRAVIS_BRANCH" = "coqdep-at-once" ]; then - UniMath_CI_GITURL=https://github.com/SkySkimmer/UniMath.git -fi diff --git a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh deleted file mode 100644 index 7e9b5febd..000000000 --- a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6324" ] || [ "$TRAVIS_BRANCH" = "fix-6323-restrict+abstract" ]; then - Equations_CI_BRANCH=fix-coq-6324 - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh b/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh deleted file mode 100644 index c0dcf79e1..000000000 --- a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6392" ] || [ "$TRAVIS_BRANCH" = "econstr+fix_class" ]; then - Equations_CI_BRANCH=econstr+fix_class - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh deleted file mode 100644 index 8aea7dee3..000000000 --- a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6413" ] || [ "$TRAVIS_BRANCH" = "interp+less_impstyle_p2" ]; then - Equations_CI_BRANCH=interp+less_impstyle_p2 - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git -fi |