From: Mark Wielaard <mark@klomp.org>
Date: Wed, 13 May 2020 13:13:18 +0000 (+0200)
Subject: dh-manual.xml: Remove duplicate dh-manual.options id.
X-Git-Tag: VALGRIND_3_16_0~29
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=7425c1bc9678b06cd9552b99e7b397b76d6d2640;p=thirdparty%2Fvalgrind.git

dh-manual.xml: Remove duplicate dh-manual.options id.

Rename one to dh-manual.realloc.
---

diff --git a/dhat/docs/dh-manual.xml b/dhat/docs/dh-manual.xml
index bd318f563e..f9fef0d505 100644
--- a/dhat/docs/dh-manual.xml
+++ b/dhat/docs/dh-manual.xml
@@ -620,7 +620,7 @@ optimization.</para>
 </sect1>
 
 
-<sect1 id="dh-manual.options" xreflabel="Treatment of realloc">
+<sect1 id="dh-manual.realloc" xreflabel="Treatment of realloc">
 <title>Treatment of <computeroutput>realloc</computeroutput></title>
 
 <para><computeroutput>realloc</computeroutput> is a tricky function and there