Shorten the file name if too long

src/js/page-functions.js

@@ -1120,6 +1120,15 @@ document.getElementById("save-area-file").addEventListener("change", (event) =>
     var labelInitialText = label.innerHTML;
 
     var fileName = event.target.files[0].name;
+
+    /* Shorten the file name if too long */
+    if (fileName.length > 17) {
+
+        let begin = fileName.slice(0, 10);
+        let end = fileName.slice(-4);
+        fileName = `${begin}..${end}`;
+    }
+
     var fileDate = new Date(event.target.files[0].lastModified);
 
     var year = fileDate.getFullYear();