diff --git a/doc/make/travis.md b/doc/make/travis.md index d4e3f50642..040c54cd40 100644 --- a/doc/make/travis.md +++ b/doc/make/travis.md @@ -1,10 +1,14 @@ Automatic Builds at [Travis](https://travis-ci.org/) ---------------------------------------------------- -Whenever a commit is submitted to the the main repository, +When a commit is submitted to the the main repository, a service hook at github will automatically build Lean using [Travis](https://travis-ci.org/). +There is a way to prevent a push from being built. +Pushes that have either ```[ci skip]``` or ```[skip ci]``` *anywhere* in one of the +commit messages will be ignored. + Automatic builds can be enabled for any *fork* of the Lean repository. We just have to go to our fork page at github; select `settings` (it is an icon on the right hand side of the page); select `Service Hooks`; select `Travis`; and provide the required information. @@ -12,4 +16,4 @@ We must have an account at Travis. By default, build reports are sent to the [leansmt-dev](https://groups.google.com/forum/#!forum/leansmt-dev) Google group. You can change that by modifying the file [.travis.yml](../../.travis.yml) in the Lean root directory. The file contains a -`recipients:` entry. \ No newline at end of file +`recipients:` entry.