diff options
| author | Hugo Herbelin | 2019-11-21 15:40:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-06 17:31:39 +0100 |
| commit | e20f967043f140d57a8fbf80eb31f5a37f2de502 (patch) | |
| tree | 3d197646f9cf270f2160cccbdf88d50aa165d7e7 /dev | |
| parent | 490704f4b2db98f4ef15f5e380b63e49e13a418b (diff) | |
Adding overlay for Quickchick PR#145.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh b/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh new file mode 100644 index 0000000000..fb66217487 --- /dev/null +++ b/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11141" ] || [ "$CI_BRANCH" = "master+labelled-pr_lconstr-and-co" ]; then + + quickchick_CI_REF=master+adapt-coq-pr11141 + quickchick_CI_GITURL=https://github.com/herbelin/QuickChick + +fi |