function adjust_footnotes() {
    return;
    const nodes = document.querySelectorAll(".footnote")
          + document.querySelectorAll(".footnotetext");
    nodes.forEach(function (node) {
        const left = node.parentElement.position().left;
        const c = document.getElementById("text");
        const half_width = c.width() / 2.0;
        const mid = c.position().left + half_width;
        const max_width = 400;
        if (left > mid) {
            node.style.right = "0em";
            node.style.left = "auto";
        } else {
            node.style.left = "0em";
            node.style.right = "auto";
        }
        node.setAttribute("width", Math.min(max_width, half_width));
    });
}

/*
window.onload = function() {
    // This means "no animation", not "don't show the tooltip."
    console.log("tooltip: " + document.tooltip, document.getAttribute("tooltip"));
    //document.tooltip.setAttribute("hide", false);
    //document.tooltip.setAttribute("show", false);
};
*/