|
From: Mark W. <ma...@so...> - 2020-05-13 15:59:22
|
https://sourceware.org/git/gitweb.cgi?p=valgrind.git;h=7425c1bc9678b06cd9552b99e7b397b76d6d2640 commit 7425c1bc9678b06cd9552b99e7b397b76d6d2640 Author: Mark Wielaard <ma...@kl...> Date: Wed May 13 15:13:18 2020 +0200 dh-manual.xml: Remove duplicate dh-manual.options id. Rename one to dh-manual.realloc. Diff: --- dhat/docs/dh-manual.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 |