Merge branch '7.0.x' into pmd7-merge-xml-rule

docs/_includes/footer.html

@@ -1,12 +1,30 @@
 <footer>
-            <div class="row">
-                <div class="col-lg-12 footer">
-                    <p class="float-right"><img src="{{ "images/logo/pmd-logo-70px.png" }}" alt="PMD logo"/></p>
-                    <p>
-                        &copy;{{ site.time | date: "%Y"  }} {{site.company_name}}. All rights reserved. <br />
-                        {% if page.last_updated %}<span>Page last updated:</span> {{page.last_updated}}<br/>{% endif %}
-                        Site last generated: {{ site.time | date: "%b %-d, %Y"  }}
-                    </p>
-                </div>
-            </div>
+    {% if site.github_editme_path and page.editmepath != false %}
+    <hr />
+    <div>
+        This documentation is written in markdown. <br />
+        If there is something missing or can be improved, edit this page on
+        github and create a PR:
+        <a
+            target="_blank"
+            href="https://github.com/{{site.github_editme_path}}{{editmepath}}"
+            role="button"
+            ><i class="fa fa-github fa-lg"></i> Edit on GitHub</a
+        >
+    </div>
+    {% endif %}
+    <hr />
+    <div class="row">
+        <div class="col-lg-12 footer">
+            &copy;{{ site.time | date: "%Y" }} {{site.company_name}}. All rights
+            reserved. <br />
+            {% if page.last_updated %}<span>Page last updated:</span>
+            {{page.last_updated}}<br />{% endif %} Site last generated: {{
+            site.time | date: "%b %-d, %Y" }} <br />
+            <p>
+                <img src="{{ "images/logo/pmd-logo-70px.png" }}" alt="PMD
+                logo"/>
+            </p>
+        </div>
+    </div>
 </footer>

docs/_includes/header.html

@@ -0,0 +1,23 @@
+<header>
+    <div class="row">
+        <div class="col-lg-12">
+            <a href="./" role="button"
+                ><i class="fa fa-home fa-lg"></i
+            ></a>
+            » {{page.title}} {% if site.github_editme_path %} {% assign
+            editmepath = page.path %} {% if page.editmepath %} {% assign
+            editmepath = page.editmepath %} {% endif %}{% unless page.editmepath
+            == false %}
+            <a
+                target="_blank"
+                href="https://github.com/{{site.github_editme_path}}{{editmepath}}"
+                class="float-right"
+                role="button"
+                ><i class="fa fa-github fa-lg"></i> Edit on GitHub</a
+            >
+            {% endunless %} {% endif %}
+        </div>
+    </div>
+
+    <hr />
+</header>

docs/_includes/toc.html

@@ -1,5 +0,0 @@
-{% comment %}
-Note: The content of the div-element is filled by javascript. See customscripts.js.
-{% endcomment %}
-
-<div id="toc"></div>