From 7db5d79c762bef4ed9e6876807cee36fd5774e12 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Jan 2018 15:43:48 -0800 Subject: [PATCH] chore(doc/faq): typo --- doc/faq.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/faq.md b/doc/faq.md index 02fe7b6f77..25262c2ee2 100644 --- a/doc/faq.md +++ b/doc/faq.md @@ -21,7 +21,7 @@ ideas and tweaking the system. It is a research project and not a product. Things change rapidly, and we constantly break backward compatibility. Lean comes "as is", you should not expect we will fix bugs and/or add new features for your project. We have our own priorities, and will not change them to accommodate your needs. -Even if you implement a new feature or fixes a bug, we may not want to merge it because +Even if you implement a new feature or fix a bug, we may not want to merge it because it may conflict with our plans for Lean, it may not be performant, we may not want to maintain it, we may be busy, etc. If you really need this new feature or bug fix, we suggest you create your own fork and maintain it yourself.