diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-bedrock2.sh | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/08829-proj-syntax-check.sh | 5 | ||||
| -rw-r--r-- | dev/ci/user-overlays/09733-gares-quotations.sh | 6 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 2 |
4 files changed, 13 insertions, 2 deletions
diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 2d242d80a4..2ac78d3c2b 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download bedrock2 -( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make | iconv -t UTF-8 -c `#9767` ) +( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make ) diff --git a/dev/ci/user-overlays/08829-proj-syntax-check.sh b/dev/ci/user-overlays/08829-proj-syntax-check.sh new file mode 100644 index 0000000000..c04621114f --- /dev/null +++ b/dev/ci/user-overlays/08829-proj-syntax-check.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "8829" ] || [ "$CI_BRANCH" = "proj-syntax-check" ]; then + lambdaRust_CI_REF=proj-syntax-check + lambdaRust_CI_GITURL=https://github.com/SkySkimmer/lambda-rust + lambdaRust_CI_ARCHIVEURL=$lambdaRust_CI_GITURL/archive +fi diff --git a/dev/ci/user-overlays/09733-gares-quotations.sh b/dev/ci/user-overlays/09733-gares-quotations.sh new file mode 100644 index 0000000000..b17454fc4c --- /dev/null +++ b/dev/ci/user-overlays/09733-gares-quotations.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9733" ] || [ "$CI_BRANCH" = "quotations" ]; then + + ltac2_CI_REF=quotations + ltac2_CI_GITURL=https://github.com/gares/ltac2 + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index b1bfac8cc9..49251d61a1 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -22,7 +22,7 @@ If you want to build the standard libraries and plugins you should call `make -f Makefile.dune voboot`. It is usually enough to do that once per-session. -More helper targets are availabe in `Makefile.dune`, `make -f +More helper targets are available in `Makefile.dune`, `make -f Makefile.dune` will display some help. Dune places build artifacts in a separate directory `_build`; it will |