Fix #1675: add edit on github button

Author: felixmulder

docs/_config.yml

@@ -1,4 +1,5 @@
 title: Dotty Documentation
+repository_url: "http://github.com/lampepfl/dotty"
 baseurl: ""
 theme: minima
 gems:

docs/_layouts/default.html

@@ -16,6 +16,9 @@
             </a>
             <div id="content">
                 <h1>{{ page.title }}</h1>
+                <div class="edit-docs">
+                    <a href="{{site.repository_url}}/edit/master/docs/{{page.path}}">[edit on github]</a>
+                </div>
                 {{ content }}
             </div>
             <div id="toc">

docs/css/main.scss

@@ -70,6 +70,7 @@ div#container {
     }
 
     div#content {
+        position: relative;
         margin-top: $distance-top;
         width: $content-width - $toc-width;
         float: right;
@@ -150,6 +151,12 @@ div#container {
     }
 }
 
+div.edit-docs {
+    position: absolute;
+    top: 8px;
+    right: 0;
+}
+
 h1#search {
     margin-top: 50px;
 }