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>