diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html
index 955164a3..8658aefa 100644
--- a/docs/_layouts/default.html
+++ b/docs/_layouts/default.html
@@ -1,5 +1,5 @@
-
+
@@ -8,6 +8,7 @@
{% seo %}
+
@@ -15,7 +16,5 @@
{{ content }}
-
-
diff --git a/docs/links.js b/docs/links.js
new file mode 100644
index 00000000..487907b9
--- /dev/null
+++ b/docs/links.js
@@ -0,0 +1,44 @@
+"use strict";
+
+
+function add_header_links()
+{
+ let style = document.createElement("style");
+ style.id = "headerlinks"
+ document.head.appendChild(style);
+ style.sheet.insertRule(
+ "a.headerlink {" +
+ " visibility: hidden;" +
+ " text-decoration: none;" +
+ " font-size: 0.8em;" +
+ " padding: 0 4px 0 4px;" +
+ "}");
+ style.sheet.insertRule(
+ ":hover > a.headerlink {" +
+ " visibility: visible;" +
+ "}");
+
+ let headers = document.querySelectorAll("h2, h3, h4, h5, h6");
+ for (let i = 0, len = headers.length; i < len; ++i)
+ {
+ let header = headers[i];
+
+ let id = header.id || header.parentNode.id;
+ if (!id)
+ continue;
+
+ let link = document.createElement("a");
+ link.href = "#" + id;
+ link.className = "headerlink";
+ link.textContent = "ΒΆ";
+
+ header.appendChild(link);
+ }
+}
+
+
+if (document.readyState !== "loading") {
+ add_header_links();
+} else {
+ document.addEventListener("DOMContentLoaded", add_header_links);
+}