/** * @file Inserts the contents of remote files into the document. * * @licstart The following is the entire license notice for the JavaScript code * in this page. * * Copyright (C) 2026 Madison L. * * The JavaScript code in this page is free software: you can redistribute it * and/or modify it under the terms of the GNU General Public License (GNU GPL) * as published by the Free Software Foundation, either version 3 of the * License, or (at your option) any later version. The code is distributed * WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or * FITNESS FOR A PARTICULAR PURPOSE. See the GNU GPL for more details. * * As additional permission under GNU GPL version 3 section 7, you may * distribute non-source (e.g., minimized or compacted) forms of that code * without the copy of the GNU GPL normally required by section 4, provided you * include this license notice and a URL through which recipients can access the * Corresponding Source. * * @licend The above is the entire license notice for the JavaScript code in * this page. * * @warning This script should only execute AFTER the document has been parsed. * Otherwise, some directives may not be processed. To avoid this, import this * script with the 'defer' attribute. */ async function processDirectives() { for (var element of document.getElementsByTagName("*")) { var path = element.getAttribute("include"); if (!path) continue; await fetch(path) .then(response => { if (!response.ok) throw new Error(`Fetching '${path}' failed`); return response.text(); }).then(contents => { element.innerHTML = contents; }).catch(error => { console.error(error); element.innerHTML = `

${error}

`; }); } } processDirectives();