diff --git a/public/js/extra.js b/public/js/extra.js
index 810d61463..23944a175 100644
--- a/public/js/extra.js
+++ b/public/js/extra.js
@@ -909,7 +909,7 @@ export function deduplicatedHeaderId (view) {
     // all headers contained in the document, in order of appearance
     const allHeaders = view.find(`:header`).toArray()
     // list of finaly assigned header IDs
-    let headerIds = new Set()
+    const headerIds = new Set()
     for (let j = 0; j < allHeaders.length; j++) {
       const $header = $(allHeaders[j])
       const id = $header.attr('id')