diff options
Diffstat (limited to 'dev/ci')
4 files changed, 22 insertions, 1 deletions
diff --git a/dev/ci/ci-coqtail.sh b/dev/ci/ci-coqtail.sh index b8b5c6c724..ab538ecc07 100755 --- a/dev/ci/ci-coqtail.sh +++ b/dev/ci/ci-coqtail.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download coqtail -( cd "${CI_BUILD_DIR}/coqtail" && PYTHONPATH=python python3 -m pytest tests/test_coqtop.py ) +( cd "${CI_BUILD_DIR}/coqtail" && PYTHONPATH=python python3 -m pytest tests/coq ) diff --git a/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh b/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh new file mode 100644 index 0000000000..7c04608403 --- /dev/null +++ b/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12565" ] || [ "$CI_BRANCH" = "fix-tc-search-opacity" ]; then + + coqhammer_CI_REF=fix-tc-search-opacity + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + +fi 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/12756-jashug-dont-refresh-argument-names.sh b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh new file mode 100644 index 0000000000..54fdd87566 --- /dev/null +++ b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "12756" ] || [ "$CI_BRANCH" = "dont-refresh-argument-names" ]; then + + mathcomp_CI_REF=dont-refresh-argument-names-overlay + mathcomp_CI_GITURL=https://github.com/jashug/math-comp + + oddorder_CI_REF=dont-refresh-argument-names-overlay + oddorder_CI_GITURL=https://github.com/jashug/odd-order + +fi |