path: root/docs/_layouts/default.html


          
<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>
<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>