summaryrefslogtreecommitdiff
path: root/src/common/doc/header.html
diff options
context:
space:
mode:
authorGard Spreemann <gspr@nonempty.org>2022-01-14 09:15:35 +0100
committerGard Spreemann <gspr@nonempty.org>2022-01-14 09:15:35 +0100
commitdbc404626955aee632fa47ee7a4d4c3add7d6188 (patch)
treeb7acfc83c9ba316216a93e9a7d14c68c11d92804 /src/common/doc/header.html
parent2c221bfcf8effff9b010de8b2e13a22f6bc15201 (diff)
parent17c3c6a07cdb1b4d4f735f3bc996af30e216dfbe (diff)
Merge tag 'tags/gudhi-release-3.5.0' into dfsg/latest
Diffstat (limited to 'src/common/doc/header.html')
-rw-r--r--src/common/doc/header.html1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/common/doc/header.html b/src/common/doc/header.html
index 9da20bbc..7c20478b 100644
--- a/src/common/doc/header.html
+++ b/src/common/doc/header.html
@@ -49,6 +49,7 @@ $extrastylesheet
<li><a href="/relatedprojects/">Related projects</a></li>
<li><a href="/theyaretalkingaboutus/">They are talking about us</a></li>
<li><a href="/inaction/">GUDHI in action</a></li>
+ <li><a href="/etymology/">Etymology</a></li>
</ul>
</li>
<li class="divider"></li>