From da1fc03d152763fb0ef41e04cc9ca5b324137709 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 29 Oct 2017 15:55:22 -0400 Subject: [PATCH] doc(CONTRIBUTING): add instructions to run test suite --- .github/CONTRIBUTING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index 84edcde8de..40eca38401 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -27,7 +27,7 @@ So, here are some guidelines for submitting PRs: - Small bug fixes are always welcome. - Before implementing a major feature or refactoring the code, please ask whether the change is welcome or not. The worst kind of PR is the "unwanted one". That is, we don’t want it, but we have to explain why we will not merge it. -- Ensure all test suite works before submitting a PR. +- Ensure all test suite works before submitting a PR. You can run the test suite (after building Lean and the Lean library) by calling `ctest` in your build directory. - Ensure your Pull Request meets the coding and commit conventions documented above. - Ensure your Pull Request contains tests for the behavior, for both features or bug fixes.