diff options
| author | Pierre-Marie Pédrot | 2018-11-17 19:04:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-17 19:04:24 +0100 |
| commit | 7d78085e47ec375c23546dfe5df9eb1b4b7d0f39 (patch) | |
| tree | 8722726b471087faf680769123274e4974841fa3 /dev | |
| parent | 71938f0de10e1f3b69b1158b80b4898bf3a7dfdb (diff) | |
| parent | 4e9bc09df64cd15e85c19ecabbc9580c00771176 (diff) | |
Merge PR #8914: [CoqProject] Abstract warning function for CoqProject readers.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh new file mode 100644 index 0000000000..1c5157ba12 --- /dev/null +++ b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8914" ] || [ "$CI_BRANCH" = "lib+better_boot_coqproject" ]; then + + quickchick_CI_REF=lib+better_boot_coqproject + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi |