diff options
author | Vincent Rouvreau <vincent.rouvreau@inria.fr> | 2022-03-08 10:40:01 +0100 |
---|---|---|
committer | Vincent Rouvreau <vincent.rouvreau@inria.fr> | 2022-03-08 10:40:01 +0100 |
commit | 6cb016c0ceff231c001928f641d344fc92c44b73 (patch) | |
tree | 5521dc1396347616a3644f96e6a9f96845c593e1 /src/common/doc/header.html | |
parent | 69168e8ed24165ab89ea1c57bc21dd994c93dd8e (diff) | |
parent | bbff86f1218fc7bc9976353901aa94cfa54792f6 (diff) |
Merge master and resolve commits
Diffstat (limited to 'src/common/doc/header.html')
-rw-r--r-- | src/common/doc/header.html | 1 |
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> |