summaryrefslogtreecommitdiff
path: root/src/common/doc
diff options
context:
space:
mode:
authorVincent Rouvreau <10407034+VincentRouvreau@users.noreply.github.com>2021-08-12 17:28:30 +0200
committerGitHub <noreply@github.com>2021-08-12 17:28:30 +0200
commit19b7d011ee20066ea6895387e0f68d3dd789e0ee (patch)
treed3f7081204cbdf33e143588399dfc93d952e5d6d /src/common/doc
parent56f79346dcdf87a462ca68188c43ec75bb61273b (diff)
parent50d7eb5bc89900dd90f7f2d97ca8bc3c19c8a057 (diff)
Merge pull request #506 from VincentRouvreau/test_another_sphinx_themes
Test another sphinx themes
Diffstat (limited to 'src/common/doc')
-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>