From d7fd8af1d5114aad148ea2530bfa6d90239f6454 Mon Sep 17 00:00:00 2001
From: Lars Hvam <larshp@hotmail.com>
Date: Mon, 7 Oct 2019 22:48:28 -0700
Subject: [PATCH] docs: add anchored links, closes #2756 (#2951)

---
 docs/_layouts/default.html | 33 +++++++++++++++++++++++++++++++++
 docs/assets/main.css       |  5 +++++
 2 files changed, 38 insertions(+)

diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html
index 14ff3f650..9c38b4689 100644
--- a/docs/_layouts/default.html
+++ b/docs/_layouts/default.html
@@ -14,5 +14,38 @@
   </div>
 </div>
 {% include footer.html %}
+
+<script type="text/javascript">
+  (function(){
+    'use strict';
+
+    /*
+    Create intra-page links
+    Requires that your headings already have an `id` attribute set (because that's what jekyll does)
+    For every heading in your page, this adds a little anchor link `#` that you can click to get a permalink to the heading.
+    Ignores `h1`, because you should only have one per page.
+    The text content of the tag is used to generate the link, so it will fail "gracefully-ish" if you have duplicate heading text.
+     */
+
+    var headingNodes = [], results, link,
+        tags = ['h2', 'h3', 'h4'];
+
+    tags.forEach(function(tag){
+      results = document.getElementsByTagName(tag);
+      Array.prototype.push.apply(headingNodes, results);
+    });
+
+    headingNodes.forEach(function(node){
+      link = document.createElement('a');
+      link.className = 'anchor-link';
+      link.textContent = '#';
+      link.href = '#' + node.getAttribute('id');
+      if (node.getAttribute('id')) {
+       node.appendChild(link);
+      }
+    });
+
+  })();
+</script>
 </body>
 </html>
diff --git a/docs/assets/main.css b/docs/assets/main.css
index a54a0ce35..1999efd32 100644
--- a/docs/assets/main.css
+++ b/docs/assets/main.css
@@ -116,3 +116,8 @@ footer.nav-footer {
 .nav-refs a {
   color: #808080;
 }
+
+.anchor-link {
+  margin-left: 5px;
+  font-size: 80%;
+}
\ No newline at end of file