aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-12-26 12:51:27 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-12-26 12:51:27 +0100
commitb9f72bf53c831bd93d28760eefdab9ad8ffdac03 (patch)
treed4f17154717e2d0dbaa705d29808706b1ed79389
parentdea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff)
Delete old overlays (leaving example)
-rw-r--r--dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh9
-rw-r--r--dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh4
-rw-r--r--dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh4
-rw-r--r--dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh4
-rw-r--r--dev/ci/user-overlays/06217-coqdep-at-once.sh3
-rw-r--r--dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh4
-rw-r--r--dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh4
-rw-r--r--dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh4
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