From 0069e9c062c80ac6ae48eaad5c361da08d8ecb93 Mon Sep 17 00:00:00 2001
From: Rene Rivera <grafikrobot@gmail.com>
Date: Mon, 23 Oct 2017 22:47:55 -0500
Subject: [PATCH] Revert "Add adoc generated tool docs to main manual."

This reverts commit 5db50e9fd892535f28d055d0eb0f3baaabe01839.
---
 doc/src/userman.xml | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/doc/src/userman.xml b/doc/src/userman.xml
index 2d8ab7d79..d798456df 100644
--- a/doc/src/userman.xml
+++ b/doc/src/userman.xml
@@ -18,12 +18,6 @@
   <xi:include href="extending.xml"/>
   <xi:include href="faq.xml"/>
 
-  <!-- Tools -->
-  <appendix id="extra-tools">
-    <title>Extra Tools</title>
-    <xi:include href="tools.docbook" parse="xml"
-      xpointer="xpointer(id('_documentation_tools')|id('_documentation_tools')/following-sibling::*)"/>
-  </appendix>
   <!-- Appendicies -->
   <appendix id="examples">
     <title>Examples</title>