docs: Make index link point to "index.html" irrespective of port.

pull/1357/head
Damien George 2015-06-27 13:41:24 +01:00
rodzic 9896314f5b
commit 8cc8f280eb
1 zmienionych plików z 4 dodań i 0 usunięć

Wyświetl plik

@ -1,2 +1,6 @@
{% extends "!layout.html" %}
{% set css_files = css_files + ["_static/customstyle.css"] %}
{# we change the master_doc variable so that links to the index
page are to index.html instead of <port>_index.html #}
{% set master_doc = "index" %}