diff options
| author | Hugo Herbelin | 2020-02-28 05:14:18 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-22 15:02:43 +0100 |
| commit | 8b8a612940127084d0162408eda5a1fe77365e79 (patch) | |
| tree | 52d81fff06c5902deb03ec83a1247166a05e2bea /dev | |
| parent | b0d34aa8cb8b0b84d6749312553d5d03709cf5f6 (diff) | |
Overlay for QuickChick
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh new file mode 100644 index 0000000000..8a734feada --- /dev/null +++ b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11703" ] || [ "$CI_BRANCH" = "master+turning-numTok-into-a-numeral-API" ]; then + + quickchick_CI_REF=master+adapting-numTok-new-api-pr11703 + quickchick_CI_GITURL=https://github.com/herbelin/QuickChick + +fi |