From 8cc8f280ebaf6731e35e5862fe9d186580389d80 Mon Sep 17 00:00:00 2001
From: Damien George <damien.p.george@gmail.com>
Date: Sat, 27 Jun 2015 13:41:24 +0100
Subject: [PATCH] docs: Make index link point to "index.html" irrespective of
 port.

---
 docs/templates/layout.html | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/docs/templates/layout.html b/docs/templates/layout.html
index 8a57bff276..a6caa0bc5a 100644
--- a/docs/templates/layout.html
+++ b/docs/templates/layout.html
@@ -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" %}