1 files changed, 13 insertions, 0 deletions
diff --git a/docs/javascript/extra.js b/docs/javascript/extra.js
new file mode 100644
index 0000000..d97526b
--- /dev/null
+++ b/docs/javascript/extra.js
@@ -0,0 +1,13 @@
+document.addEventListener("DOMContentLoaded", function () {
+    document.querySelectorAll(".termynal").forEach(function (termynalEl) {
+        new Termynal(termynalEl);
+    });
+
+    // Redirect /gitlint/configuration/#regex-style-search to /gitlint/configuration/general_options/#regex-style-search
+    // 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 == "/gitlint/configuration/" && window.location.hash === "#regex-style-search") {
+        window.location.href = "/gitlint/configuration/general_options/#regex-style-search";
+    }
+});