diff options
author | Vincent Rouvreau <10407034+VincentRouvreau@users.noreply.github.com> | 2021-08-12 17:28:30 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-12 17:28:30 +0200 |
commit | 19b7d011ee20066ea6895387e0f68d3dd789e0ee (patch) | |
tree | d3f7081204cbdf33e143588399dfc93d952e5d6d /src/common | |
parent | 56f79346dcdf87a462ca68188c43ec75bb61273b (diff) | |
parent | 50d7eb5bc89900dd90f7f2d97ca8bc3c19c8a057 (diff) |
Merge pull request #506 from VincentRouvreau/test_another_sphinx_themes
Test another sphinx themes
Diffstat (limited to 'src/common')
-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> |