diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh index e2c27c939e..6bee3c7bb6 100644 --- a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh +++ b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh @@ -1,15 +1,15 @@ if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then - fiat_crypto_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file + fiat_crypto_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto - mtac2_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file + mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 - metacoq_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file + metacoq_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file metacoq_CI_GITURL=https://github.com/herbelin/template-coq - unimath_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file + unimath_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file unimath_CI_GITURL=https://github.com/herbelin/UniMath fi |