diff options
| author | hoijui | 2019-10-29 11:57:51 +0100 |
|---|---|---|
| committer | hoijui | 2019-10-30 17:46:45 +0100 |
| commit | 3233a448c6cd7f4636daf4008fe8b98d288219d0 (patch) | |
| tree | ef83daaabb0ebe27ecbf49caa3a08df17de72a73 /public/js | |
| parent | e1ff73877b5ae772489e60e3509260d0a25b01a4 (diff) | |
make `headerIds` `const` [fix]
Signed-off-by: hoijui <hoijui.quaero@gmail.com>
Diffstat (limited to 'public/js')
| -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') |