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/css | |
| 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/css')
| -rw-r--r-- | docs/css/main.scss | 7 |
1 files changed, 7 insertions, 0 deletions
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; } |