path: root/docs/_layouts/default.html



<html>
    <head>
        <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">
                {{ 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>
<html>
    <head>
        <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">
                {{ 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>