From: Tom Hughes <tom@compton.nu>
Date: Mon, 15 Aug 2011 08:20:53 +0000 (+0000)
Subject: Mention the --tool option in the manual page. Fixes #249970.
X-Git-Tag: svn/VALGRIND_3_7_0~258
X-Git-Url: http://git.ipfire.org/gitweb.cgi?a=commitdiff_plain;h=09b283bb40904e2ca0bcd72acc2858e34434ba71;p=thirdparty%2Fvalgrind.git

Mention the --tool option in the manual page. Fixes #249970.


git-svn-id: svn://svn.valgrind.org/valgrind/trunk@11979
---

diff --git a/docs/xml/manual-core.xml b/docs/xml/manual-core.xml
index de0d333d8c..1e03d66f4c 100644
--- a/docs/xml/manual-core.xml
+++ b/docs/xml/manual-core.xml
@@ -564,9 +564,9 @@ in most cases.  We group the available options by rough categories.</para>
 <sect2 id="manual-core.toolopts" xreflabel="Tool-selection Option">
 <title>Tool-selection Option</title>
 
-<para>The single most important option.</para>
+<para id="tool.opts.para">The single most important option.</para>
 
-<variablelist>
+<variablelist id="tool.opts.list">
 
   <varlistentry id="tool_name" xreflabel="--tool">
     <term>
diff --git a/docs/xml/valgrind-manpage.xml b/docs/xml/valgrind-manpage.xml
index 0d086fffe6..8f2f630751 100644
--- a/docs/xml/valgrind-manpage.xml
+++ b/docs/xml/valgrind-manpage.xml
@@ -49,6 +49,19 @@ system: <filename>&vg-docs-path;</filename>, or online:
 
 
 
+<refsect1 id="tool-selection-options">
+<title>Tool Selection Options</title>
+
+<xi:include href="manual-core.xml" xpointer="tool.opts.para"
+            xmlns:xi="http://www.w3.org/2001/XInclude" />
+
+<xi:include href="manual-core.xml" xpointer="tool.opts.list"
+            xmlns:xi="http://www.w3.org/2001/XInclude" />
+
+</refsect1>
+
+
+
 <refsect1 id="basic-options">
 <title>Basic Options</title>