diff --git a/docs/assets/hide_turing_menu.js b/docs/assets/hide_turing_menu.js new file mode 100644 index 000000000..5a27c459d --- /dev/null +++ b/docs/assets/hide_turing_menu.js @@ -0,0 +1,22 @@ +// Remove the Turing navigation menu from the documentation pages, +// if present. Tested against the navbar code defined in +// https://github.com/TuringLang/turinglang.github.io/blob/3e4f5900d90e014a939867e3fe1ac256bdd37f14/assets/scripts/TuringNavbar.html +document.addEventListener("DOMContentLoaded", function () { + var navElement = document.querySelector('nav.ext-navigation'); + if (navElement) { + // Remove the