From e43461e841bb8a92fca7414013d88319b9b84ed5 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 18 Jun 2018 11:08:25 +0200 Subject: Update section on adding your project to CI and link to example PR. --- dev/ci/README.md | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) (limited to 'dev') diff --git a/dev/ci/README.md b/dev/ci/README.md index 665b3768a..08364c897 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -47,16 +47,13 @@ CI. ### Add your development by submitting a pull request -Add a new `ci-mydev.sh` script to [`dev/ci`](.) (have a look at -[`ci-coq-dpdgraph.sh`](ci-coq-dpdgraph.sh) or -[`ci-fiat-parsers.sh`](ci-fiat-parsers.sh) for simple examples); -set the corresponding variables in -[`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the corresponding -target to [`Makefile.ci`](../../Makefile.ci); add new jobs to -[`.gitlab-ci.yml`](../../.gitlab-ci.yml), -[`.circleci/config.yml`](../../.circleci/config.yml) and -[`.travis.yml`](../../.travis.yml) so that this new target is run. **Do not -hesitate to submit an incomplete pull request if you need help to finish it.** +Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding +variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the +corresponding target to [`Makefile.ci`](../../Makefile.ci) and a new job to +[`.gitlab-ci.yml`](../../.gitlab-ci.yml) so that this new target is run. +Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an +example. **Do not hesitate to submit an incomplete pull request if you need +help to finish it.** You may also be interested in having your development tested in our performance benchmark. Currently this is done by providing an OPAM package -- cgit v1.2.3