blob: 992487de8143fee7b416434cb8e59fe9034bf6e4 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
<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="{{ 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);
}
</script>
</html>
|
