summaryrefslogtreecommitdiff
path: root/src/common/doc/header.html
diff options
context:
space:
mode:
authorVincent Rouvreau <vincent.rouvreau@inria.fr>2022-03-08 10:40:01 +0100
committerVincent Rouvreau <vincent.rouvreau@inria.fr>2022-03-08 10:40:01 +0100
commit6cb016c0ceff231c001928f641d344fc92c44b73 (patch)
tree5521dc1396347616a3644f96e6a9f96845c593e1 /src/common/doc/header.html
parent69168e8ed24165ab89ea1c57bc21dd994c93dd8e (diff)
parentbbff86f1218fc7bc9976353901aa94cfa54792f6 (diff)
Merge master and resolve commits
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>