diff options
| author | Felix Mulder <felix.mulder@gmail.com> | 2016-11-07 15:57:06 +0100 |
|---|---|---|
| committer | Felix Mulder <felix.mulder@gmail.com> | 2016-11-07 15:58:08 +0100 |
| commit | f179c9279f9f9a3bf9ef342900590e761855a696 (patch) | |
| tree | c47f3e43d14d8265cd3bedbd2aafe84441f310e8 /docs | |
| parent | e1f2ce54cdad3cc2b11070dbf9e288ce34f5e731 (diff) | |
| download | dotty-f179c9279f9f9a3bf9ef342900590e761855a696.tar.gz dotty-f179c9279f9f9a3bf9ef342900590e761855a696.tar.bz2 dotty-f179c9279f9f9a3bf9ef342900590e761855a696.zip | |
Fix #1675: add `edit on github` button
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/_config.yml | 1 | ||||
| -rw-r--r-- | docs/_layouts/default.html | 3 | ||||
| -rw-r--r-- | docs/css/main.scss | 7 |
3 files changed, 11 insertions, 0 deletions
diff --git a/docs/_config.yml b/docs/_config.yml index 51578256b..1bdfb808a 100644 --- a/docs/_config.yml +++ b/docs/_config.yml @@ -1,4 +1,5 @@ title: Dotty Documentation +repository_url: "http://github.com/lampepfl/dotty" baseurl: "" theme: minima gems: diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html index 65a2cd859..992487de8 100644 --- a/docs/_layouts/default.html +++ b/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"> diff --git a/docs/css/main.scss b/docs/css/main.scss index 2fca7d8ea..43da29284 100644 --- a/docs/css/main.scss +++ b/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; } |