docs/javascript/extra.js


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

document.addEventListener("DOMContentLoaded", function () {
    document.querySelectorAll(".termynal").forEach(function (termynalEl) {
        new Termynal(termynalEl);
    });

    // Redirect /gitlint/configuration/#<option> to /gitlint/configuration/general_options/#<option>
    // This is to support old links that are in gitlint's CLI Output
    // If the trailing slash is missing from /gitlint/configuration, mkdocs will redirect to the trailing slash version,
    // and then this code will redirect to the correct page
    if (window.location.pathname.endsWith("configuration/")) {
        if (window.location.hash === "#regex-style-search") {
            window.location.href = "/gitlint/configuration/general_options/#regex-style-search";
        } else if (window.location.hash === "#staged") {
            window.location.href = "/gitlint/configuration/general_options/#staged";
        }
    }
});