diff --git a/src/gui/theming.js b/src/gui/theming.js index 038a21fcf6d06b9441daf2852408d1fbf375dafe..08bf7e627f8175d8e1be77badcc6279bf2febc44 100644 --- a/src/gui/theming.js +++ b/src/gui/theming.js @@ -45,10 +45,7 @@ App.UI.Theme = (function() { */ function load(filename) { V.theme = filename; - currentThemeElement = newTheme(filename); - - document.head.appendChild(currentThemeElement); } function unload() { @@ -71,16 +68,22 @@ App.UI.Theme = (function() { if (filename !== undefined) { devTheme = newTheme(filename); - - document.head.appendChild(devTheme); + // make it unique to force reloading instead of using the cached version + devTheme.href += `?id=${Date.now()}`; } } + /** + * Creates an new theme and adds it to the head element + * @param {string} filename + * @returns {HTMLLinkElement} + */ function newTheme(filename) { const theme = document.createElement("link"); theme.setAttribute("rel", "stylesheet"); theme.setAttribute("type", "text/css"); theme.setAttribute("href", `./${filename}`); + document.head.appendChild(theme); return theme; }