summaryrefslogtreecommitdiff
path: root/src/common/doc/header.html
diff options
context:
space:
mode:
authorROUVREAU Vincent <vincent.rouvreau@inria.fr>2021-06-25 16:26:55 +0200
committerROUVREAU Vincent <vincent.rouvreau@inria.fr>2021-06-25 16:26:55 +0200
commitc0cca8dbd60e3da5147517f6f8f37d9bdeefe511 (patch)
tree006c79d81b350d13604c4f0b9305a2b0fa35f9c0 /src/common/doc/header.html
parentb32f61a66d52a25be177dd96de469420e5b4a980 (diff)
update headers, conf.py for the new theme and bottleneck image to be smaller
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>