diff options
| author | Hugo Herbelin | 2020-04-18 14:50:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-21 19:33:19 +0200 |
| commit | 7f4092718deed6c3d492ef3a1be16cef51212c14 (patch) | |
| tree | 0bf81246329e88d7fe5fdfe0ac5a45acfe32dffd /dev/ci | |
| parent | cc0aa0d6e9a8fafbd42c90cdfda8e9be590c03cb (diff) | |
Overlay for fiat-crypto, Mtac2, MetaCoq and UniMath.
Diffstat (limited to 'dev/ci')
| -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 |