From d5c7f91b836a63fc839a7abb9a0b2620245ff77f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Nov 2020 09:58:51 -0800
Subject: [PATCH] chore: reorg manual main page

---
 doc/SUMMARY.md | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index bef94ef8ef..1953c2ad48 100644
--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -12,8 +12,10 @@
 - [Tactics](./tactics.md)
 - [String interpolation](./stringinterp.md)
 
-# Tools
+# Other
 
+- [Frequently Asked Questions](./faq.md)
+- [Significant Changes from Lean 3](./lean3changes.md)
 - [Syntax Highlighting Lean in LaTeX](./syntax_highlight_in_latex.md)
 
 # Development
@@ -25,8 +27,3 @@
   - [Windows Setup](./make/msys2.md)
 - [Building This Manual](./mdbook.md)
 - [Fixing Tests](./fixing_tests.md)
-
-# Other
-
-- [Frequently Asked Questions](./faq.md)
-- [Significant Changes from Lean 3](./lean3changes.md)