diff options
| -rw-r--r-- | public/js/extra.js | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/public/js/extra.js b/public/js/extra.js index 810d6146..23944a17 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') |