diff options
Diffstat (limited to 'docs/_layouts')
| -rw-r--r-- | docs/_layouts/blog.html | 17 | ||||
| -rw-r--r-- | docs/_layouts/default.html | 61 | ||||
| -rw-r--r-- | docs/_layouts/index.html | 38 | ||||
| -rw-r--r-- | docs/_layouts/search.html | 17 |
4 files changed, 0 insertions, 133 deletions
diff --git a/docs/_layouts/blog.html b/docs/_layouts/blog.html deleted file mode 100644 index f476bf5fa..000000000 --- a/docs/_layouts/blog.html +++ /dev/null @@ -1,17 +0,0 @@ ---- -layout: default ---- - -<h2 class="subtitle">{{ page.subTitle }}</h2> - -<div class="author-container {% if page.authorImg != null %} spaced {% endif %}"> - {% if page.authorImg != null %} - <img src="{{ site.baseurl }}{{ page.authorImg }}"/> - {% endif %} - <div class="author-info"> - <div>{{ page.author }}</div> - <div>{{ page.date | date: '%B %d, %Y' }}</div> - </div> -</div> - -{{ content }} diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html deleted file mode 100644 index 6fa1a1d78..000000000 --- a/docs/_layouts/default.html +++ /dev/null @@ -1,61 +0,0 @@ -<html> - <head> - <meta charset="utf-8"> - - <title>Dotty - {{ page.title }}</title> - <link rel="shortcut icon" type="image/png" href="{{ site.baseurl}}/images/favicon.png"/> - <link rel="stylesheet" href="http://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.7.0/styles/github.min.css"> - <link rel="stylesheet" href="{{ site.baseurl }}/css/main.css"> - </head> - <body> - <div id="container"> - <a class="logo-container" href="{{ site.baseurl }}/"> - <div id="scala-logo-mobile"> - {% include scala-logo.html %} - </div> - </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"> - {% include toc.html %} - </div> - </div> - </body> - <script src="https://cdnjs.cloudflare.com/ajax/libs/mark.js/8.4.0/mark.min.js"></script> - <script src="{{ site.baseurl }}/js/highlight.pack.js"></script> - <script language="javascript"> - hljs.initHighlightingOnLoad(); - var x = document.links.length; - for (i = 0; i < x; i++) { - var thisHREF = document.links[i].href; - if (thisHREF.indexOf(window.location.hostname) > -1) thisHREF = thisHREF.replace(".md",".html") - document.links[i].setAttribute('href', thisHREF); - } - - function getQueryVariable(variable) { - var query = window.location.search.substring(1); - var vars = query.split('&'); - - for (var i = 0; i < vars.length; i++) { - var pair = vars[i].split('='); - - if (pair[0] === variable) { - return decodeURIComponent(pair[1].replace(/\+/g, '%20')); - } - } - } - - - var highlight = getQueryVariable("highlight"); - if (highlight) { - var context = document.querySelector("#content"); - var instance = new Mark(context); - instance.mark(highlight); - } - </script> -</html> diff --git a/docs/_layouts/index.html b/docs/_layouts/index.html deleted file mode 100644 index aeb2fa7d7..000000000 --- a/docs/_layouts/index.html +++ /dev/null @@ -1,38 +0,0 @@ -<!DOCTYPE html> -<html lang="en"> - <head> - <meta charset="utf-8"> - <meta name="theme-color" content="#de332e"> - <meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no" /> - <meta http-equiv="x-ua-compatible" content="ie=edge"> - <meta property="og:image" content="http://dotty.epfl.ch/images/preview.png" /> - - <title>Dotty</title> - - <link rel="icon" type="image/png" href="{{ site.baseurl }}/images/favicon.png"> - <link href="https://fonts.googleapis.com/icon?family=Material+Icons" rel="stylesheet"> - <link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/4.0.0-alpha.2/css/bootstrap.min.css" integrity="sha384-y3tfxAZXuh4HwSYylfB+J125MxIs6mR5FOHamPBG064zB+AFeWH94NdvaCBm8qnd" crossorigin="anonymous"> - <link rel="stylesheet" type="text/css" href="{{ site.baseurl }}/css/animate.css" /> - <link rel="stylesheet" type="text/css" href="{{ site.baseurl }}/css/default.css" /> - - <!-- Yandex.Metrika counter --> - <script type="text/javascript"> - (function (d, w, c) { (w[c] = w[c] || []).push(function() { try { w.yaCounter37916575 = new Ya.Metrika({ id:37916575, clickmap:true, trackLinks:true, accurateTrackBounce:true, webvisor:true, trackHash:true }); } catch(e) { } }); var n = d.getElementsByTagName("script")[0], s = d.createElement("script"), f = function () { n.parentNode.insertBefore(s, n); }; s.type = "text/javascript"; s.async = true; s.src = "https://mc.yandex.ru/metrika/watch.js"; if (w.opera == "[object Opera]") { d.addEventListener("DOMContentLoaded", f, false); } else { f(); } }) - (document, window, "yandex_metrika_callbacks"); - </script> - <noscript><div><img src="https://mc.yandex.ru/watch/37916575" style="position:absolute; left:-9999px;" alt /></div></noscript> <!-- /Yandex.Metrika counter --> - - <script src="https://ajax.googleapis.com/ajax/libs/jquery/2.1.4/jquery.min.js" defer></script> - <script src="https://maxcdn.bootstrapcdn.com/bootstrap/4.0.0-alpha.2/js/bootstrap.min.js" integrity="sha384-vZ2WRJMwsjRMW/8U7i6PWi6AlO1L79snBrmgiDpgIWJ82z8eA5lenwvxbMV1PAh7" crossorigin="anonymous" defer></script> - <script src="https://cdn.jsdelivr.net/scrollreveal.js/3.1.4/scrollreveal.min.js" defer></script> - <script src="{{ site.baseurl }}/js/index.js" defer></script> - </head> - <body> - <div id="content"> - {% include logo-page.html %} - {% include faq.html %} - {% include features.html %} - {% include getting-started.html %} - </div> - </body> -</html> diff --git a/docs/_layouts/search.html b/docs/_layouts/search.html deleted file mode 100644 index 14994ab62..000000000 --- a/docs/_layouts/search.html +++ /dev/null @@ -1,17 +0,0 @@ -<html> - <head> - <meta charset="utf-8"> - - <title>Dotty - {{ page.title }}</title> - <link rel="shortcut icon" type="image/png" href="{{ site.baseurl}}/images/favicon.png"/> - <link rel="stylesheet" href="http://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.7.0/styles/github.min.css"> - <link rel="stylesheet" href="{{ site.baseurl }}/css/main.css"> - </head> - <body> - <div id="container"> - <div class="search"> - {{ content }} - </div> - </div> - </body> -</html> |