From a5d63f3ef06f7543cb0b0a6174a3706b4a204001 Mon Sep 17 00:00:00 2001
From: Arnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Date: Wed, 6 Feb 2019 23:13:25 +0100
Subject: [PATCH] Fix generation of graphical-toc.svg.

Attribute target="_top" was duplicated on line 6120.
---
 docs/Build.sh | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/docs/Build.sh b/docs/Build.sh
index b9b55f2c60..4096cfdaad 100755
--- a/docs/Build.sh
+++ b/docs/Build.sh
@@ -32,10 +32,8 @@ PYTHONPATH=../lib sphinx-build -M html source build ${SPHINXOPTS}
 
 set +x
 
-< source/img/graphical-toc.svg \
-   perl -pe 's/(xlink:href="http)/target="_top" $1/' \
- | perl -pe 's/(xlink:href=".*?.html)/target="_top" $1/' \
- > build/html/graphical-toc.svg
+perl -pe 's/(xlink:href="(?:http|.*\.html))/target="_top" $1/' \
+     source/img/graphical-toc.svg > build/html/graphical-toc.svg
 
 echo "List of missing references:"
 for f in $( (grep '<name>' build/xml/msg_8h.xml; \
-- 
2.20.1