diff -r f81fe8250ed9 -r 20adaa127663 misc/graves_js_anim.xhtml
--- a/misc/graves_js_anim.xhtml	Thu Aug 24 20:12:28 2023 +0200
+++ b/misc/graves_js_anim.xhtml	Thu Aug 24 20:15:40 2023 +0200
@@ -61,8 +61,8 @@
     </style>
     <script type="application/ecmascript">
 //<![CDATA[
-var IS_LOCAL=false; // set to true to fetch graves locally. Useful for testing.
-var graves;
+let IS_LOCAL=false; // set to true to fetch flags locally. Useful for testing.
+let graves;
 if (IS_LOCAL) {
 /* JavaScript version of a sprite sheet - this could be pretty trivially done in pure HTML, but maintenance
 would be easier with a server-side portion. list of sprites could be gotten from server, but would require XSS whitelisting */
@@ -78,7 +78,7 @@
 graves = [];
 }
 
-var themes = {
+let themes = {
 // Last updated: 1.0.0
 "Art":1,
 "Beach":1,
@@ -113,14 +113,14 @@
 "Snow":1,
 "Stage":1,
 "Underwater":1};
-var girder;
-var animationInterval;
+let girder;
+let animationInterval;
 
 on_xml_loaded = function(ex)
 {
-    var resp = this.responseText;
-    var r = />([^<]*).png</g;
-    var x;
+    let resp = this.responseText;
+    let r = />([^<]*).png</g;
+    let x;
     while(x = r.exec(resp))
     {
         graves.push(x[1]);
@@ -130,7 +130,7 @@
 
 on_xml_error = function()
 {
-    var p = document.createElement("p");
+    let p = document.createElement("p");
     p.appendChild(document.createTextNode("ERROR: List of graves could not be fetched from the server!"));
     document.body.appendChild(p);
 }
@@ -140,7 +140,7 @@
     // Load list of graves
     if (!IS_LOCAL) {
         // Request list of graves from repository URL
-        var xml=new XMLHttpRequest();
+        let xml=new XMLHttpRequest();
         xml.open("GET", "//hg.hedgewars.org/hedgewars/file/tip/share/hedgewars/Data/Graphics/Graves/");
         xml.addEventListener("error", on_xml_error);
         xml.onload = on_xml_loaded;
@@ -155,28 +155,28 @@
 on_graves_loaded = function()
 {
     // Render girders
-    var s = document.styleSheets[0].cssRules;
-    for(var i=0;i<s.length;i++)
+    let s = document.styleSheets[0].cssRules;
+    for(let i=0;i<s.length;i++)
     {
         if (s[i].selectorText.toLowerCase() === ".girder")
             girder = s[i];
     }
 
-    var a = document.createElement("a");
-    var g = document.createElement("div");
+    let a = document.createElement("a");
+    let g = document.createElement("div");
     g.className="girder";
     a.className="grave";
     a.appendChild(document.createElement("div"));
     a.lastChild.appendChild(document.createTextNode(""));
 
     // Render graves
-    var missingGraves = [];
-    var img;
-    var j = 0;
-    var toDelete = [];
-    for (var i=0;i<graves.length;i++)
+    let missingGraves = [];
+    let img;
+    let j = 0;
+    let toDelete = [];
+    for (let i=0;i<graves.length;i++)
     {
-        var h = document.body.appendChild(a.cloneNode(true));
+        let h = document.body.appendChild(a.cloneNode(true));
         if (IS_LOCAL)
             h.href = "../share/hedgewars/Data/Graphics/Graves/"+graves[i]+".png";
         else
@@ -194,20 +194,20 @@
     animationInterval = setInterval(animateGraves, 128);
 
     // Theme selection drop-down list
-    var form = document.body.appendChild(document.createElement("form"));
+    let form = document.body.appendChild(document.createElement("form"));
 
-    var opt = document.createElement("option");
+    let opt = document.createElement("option");
     opt.appendChild(document.createTextNode(""));
 
-    var label = document.createElement("label");
+    let label = document.createElement("label");
     label.htmlFor = "theme_select";
     label.appendChild(document.createTextNode("Theme: "));
     form.appendChild(label);
 
-    var sel = form.appendChild(document.createElement("select"));
+    let sel = form.appendChild(document.createElement("select"));
     sel.id = "theme_select";
     sel.onchange = switchTheme;
-    for(var theme in themes)
+    for(let theme in themes)
     {
         sel.appendChild(opt.cloneNode(true));
         sel.lastChild.value = theme;
@@ -218,7 +218,7 @@
     form.appendChild(document.createElement("br"));
 
     // Checkbox: Switch animation
-    var chk = document.createElement("input");
+    let chk = document.createElement("input");
     chk.id = "anim";
     chk.type = "checkbox";
     chk.onclick = switchAnim;
@@ -250,14 +250,14 @@
 
 function animateGraves()
 {
-    var a = document.getElementsByTagName("a");
-    for (var i=0;i<a.length;i++)
+    let a = document.getElementsByTagName("a");
+    for (let i=0;i<a.length;i++)
     {
         if (a[i].className !== "grave")
             continue;
         // Cycle thru animation frames
 
-        var maskName = a[i].title;
+        let maskName = a[i].title;
         // Grave
         a[i].firstChild.style.backgroundPosition=Math.floor(a[i].idle/16)*-32+"px "+(a[i].idle%16)*-32+"px";
 
@@ -282,8 +282,8 @@
 // Turn on or off girders
 function hideGirders()
 {
-    var g = document.getElementsByClassName("girder");
-    for(var i=0;i<g.length;i++)
+    let g = document.getElementsByClassName("girder");
+    for(let i=0;i<g.length;i++)
         if (this.checked)
             g[i].className = "girder";
         else
@@ -294,12 +294,12 @@
 // Select theme according to drop-down list value
 function switchTheme()
 {
-    var prefix;
+    let prefix;
     if (!IS_LOCAL)
         prefix = "//hg.hedgewars.org/hedgewars/raw-file/tip";
     else
         prefix = "..";
-    var theme = this.value || "Nature";
+    let theme = this.value || "Nature";
     document.body.style.backgroundImage='url("'+prefix+'/share/hedgewars/Data/Themes/'+theme+'/Sky.png")';
     if (themes[theme])
         girder.style.backgroundImage='url("'+prefix+'/share/hedgewars/Data/Themes/'+theme+'/Girder.png")';