function set_link_listeners() {
    Array.from(document.getElementsByClassName("pagelink")).forEach(
        function (elt) {
            elt.addEventListener("click", function(event) {
                let basename = elt.getAttribute("data-page");
                let id = elt.getAttribute("data-id");
                go_to_section(elt, basename, id);
            });
        });
}