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 bd318f563e248aaaf9c85a3b17e034ca35c06440..f9fef0d505e0b6f927c2f736b5bcf56a84cf2883 100644 (file)
--- 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