Merge PR #6809: Improve shell scripts

15 files changed, 4 insertions, 102 deletions

diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
index 7716bcb59a..e9ba114148 100644
--- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
+++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
@@ -1,3 +1,5 @@
+#!/bin/sh
+
 if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
     mathcomp_CI_BRANCH=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
diff --git a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh
deleted file mode 100644
index c2e3670380..0000000000
--- a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6405" ] || [ "$CI_BRANCH" = "rm-local-polymorphic-flag" ]; then
-    Equations_CI_BRANCH=rm-local-polymorphic-flag
-    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh
deleted file mode 100644
index 78789a6fc5..0000000000
--- a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then
-    HoTT_CI_BRANCH=check-poly-effects
-    HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git
-fi
diff --git a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh
deleted file mode 100644
index 9677b35253..0000000000
--- a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6493" ] || [ "$CI_BRANCH" = "API/remove-big-file" ]; then
-    Equations_CI_BRANCH=API-removal
-    Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git
-    coq_dpdgraph_CI_BRANCH=API-removal
-    coq_dpdgraph_CI_GITURL=https://github.com/gares/coq-dpdgraph.git
-    ltac2_CI_BRANCH=API-removal
-    ltac2_CI_GITURL=https://github.com/gares/ltac2.git
-fi
diff --git a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh
deleted file mode 100644
index 4b681909d6..0000000000
--- a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh
+++ /dev/null
@@ -1,7 +0,0 @@
- if [ "$CI_PULL_REQUEST" = "6511" ] || [ "$CI_BRANCH" = "econstr+more_fix" ]; then
-    ltac2_CI_BRANCH=econstr+more_fix
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    Equations_CI_BRANCH=econstr+more_fix
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh
deleted file mode 100644
index 8a50fb1111..0000000000
--- a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6535" ] || [ "$CI_BRANCH" = "fix-push-rel-to-named" ]; then
-    Equations_CI_BRANCH=fix-6535
-    Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh
deleted file mode 100644
index 2451657d43..0000000000
--- a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6676" ] || [ "$CI_BRANCH" = "proofview/goal-w-state" ]; then
-    ltac2_CI_BRANCH=fix-for/6676
-    ltac2_CI_GITURL=https://github.com/gares/ltac2.git
-    Equations_CI_BRANCH=fix-for/6676
-    Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/06686-ccnv-no-proj.sh b/dev/ci/user-overlays/06686-ccnv-no-proj.sh
deleted file mode 100644
index 3a3ab44e03..0000000000
--- a/dev/ci/user-overlays/06686-ccnv-no-proj.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6686" ] || [ "$CI_BRANCH" = "ccnv-no-proj" ]; then
-    Equations_CI_BRANCH=ccnv-fixes
-    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh
deleted file mode 100644
index d1d61fec2e..0000000000
--- a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh
+++ /dev/null
@@ -1,13 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6745" ] || [ "$CI_BRANCH" = "located+vernac" ]; then
-    ltac2_CI_BRANCH=located+vernac
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    Equations_CI_BRANCH=located+vernac
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    fiat_parsers_CI_BRANCH=located+vernac
-    fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
-
-    Elpi_CI_BRANCH=located+vernac
-    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
-fi
diff --git a/dev/ci/user-overlays/06775-univ-cumul-weak.sh b/dev/ci/user-overlays/06775-univ-cumul-weak.sh
deleted file mode 100644
index 8afcbf78a3..0000000000
--- a/dev/ci/user-overlays/06775-univ-cumul-weak.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6775" ] || [ "$CI_BRANCH" = "univ-cumul" ]; then
-    Elpi_CI_BRANCH=coq-master
-    Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git
-fi
diff --git a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh b/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh
deleted file mode 100644
index df3e9cef28..0000000000
--- a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh
+++ /dev/null
@@ -1,14 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6831" ] || [ "$CI_BRANCH" = "located+vernac_2" ]; then
-
-    ltac2_CI_BRANCH=located+vernac_2
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    Equations_CI_BRANCH=located+vernac_2
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    # fiat_parsers_CI_BRANCH=located+vernac
-    # fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
-
-    Elpi_CI_BRANCH=located+vernac_2
-    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
-fi
diff --git a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh
deleted file mode 100644
index a785290e7c..0000000000
--- a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6837" ] || [ "$CI_BRANCH" = "located+libnames" ]; then
-
-    ltac2_CI_BRANCH=located+libnames
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    Equations_CI_BRANCH=located+libnames
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    Elpi_CI_BRANCH=located+libnames
-    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
-
-    coq_dpdgraph_CI_BRANCH=located+libnames
-    coq_dpdgraph_CI_GITURL=https://github.com/ejgallego/coq-dpdgraph.git
-
-fi
diff --git a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh b/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh
deleted file mode 100644
index 5dedca0ca5..0000000000
--- a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6869" ] || [ "$CI_BRANCH" = "ssr+correct_packing" ]; then
-
-    Equations_CI_BRANCH=ssr+correct_packing
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    ltac2_CI_BRANCH=ssr+correct_packing
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    Elpi_CI_BRANCH=ssr+correct_packing
-    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
-
-fi
diff --git a/dev/ci/user-overlays/06923-ppedrot-export-options.sh b/dev/ci/user-overlays/06923-ppedrot-export-options.sh
deleted file mode 100644
index 333a9e84bd..0000000000
--- a/dev/ci/user-overlays/06923-ppedrot-export-options.sh
+++ /dev/null
@@ -1,7 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6923" ] || [ "$CI_BRANCH" = "export-options" ]; then
-    ltac2_CI_BRANCH=export-options
-    ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
-
-    Equations_CI_BRANCH=export-options
-    Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 9f0377ceea..a7474e3248 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -7,6 +7,8 @@ The name of your overlay file should be of the form `five_digit_PR_number-GitHub
 Example: `00669-maximedenes-ssr-merge.sh` containing
 
 ```
+#!/bin/sh
+
 if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
     mathcomp_CI_BRANCH=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git