diff options
| author | Jason Gross | 2018-07-16 09:50:50 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-07-16 09:50:50 -0400 |
| commit | 2c96888bd26c293832f442680561fb72f9dc82f5 (patch) | |
| tree | 4dfb4e431691bb61c1d9a2e48bbbe7445e77ebb8 /dev/ci | |
| parent | 7f7e567188ea40fb396c1802224b7290b9e873a3 (diff) | |
Add overlay for QuickChick
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/08063-jasongross-string-eqb.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/08063-jasongross-string-eqb.sh b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh new file mode 100644 index 0000000000..99a11b9fbf --- /dev/null +++ b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8063" ] || [ "$CI_BRANCH" = "string-eqb" ]; then + quickchick_CI_BRANCH=fix-for-pr-8063 + quickchick_CI_GITURL=https://github.com/JasonGross/QuickChick +fi |