diff options
Diffstat (limited to 'dev/ci')
| -rwxr-xr-x | dev/ci/ci-metacoq.sh | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh | 6 | ||||
| -rw-r--r-- | dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh | 6 |
3 files changed, 13 insertions, 1 deletions
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 1302065961..27876d68de 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download metacoq -( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install ) +( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make .merlin && make ci-local && make install ) diff --git a/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh b/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh new file mode 100644 index 0000000000..56a69abbf7 --- /dev/null +++ b/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12709" ] || [ "$CI_BRANCH" = "hint-pattern-out" ]; then + + coqhammer_CI_REF=hint-pattern-out + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + +fi diff --git a/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh new file mode 100644 index 0000000000..e57f95ef19 --- /dev/null +++ b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12720" ] || [ "$CI_BRANCH" = "factor-class-hint-clenv" ]; then + + coqhammer_CI_REF=factor-class-hint-clenv + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + +fi |