Fix invalid lint ID filtering

GuillaumeGomez · GuillaumeGomez · commit b33977b8520b · 2024-10-22T22:54:29.000+02:00
diff --git a/util/gh-pages/script.js b/util/gh-pages/script.js
@@ -512,7 +512,7 @@ function scrollToLint(lintId) {
 
 // If the page we arrive on has link to a given lint, we scroll to it.
 function scrollToLintByURL() {
-    const lintId = window.location.hash.substring(2);
+    const lintId = window.location.hash.substring(1);
     if (lintId.length > 0) {
         scrollToLint(lintId);
     }

Original file line number	Diff line number	Diff line change
`@@ -512,7 +512,7 @@ function scrollToLint(lintId) {`
`512`	`512`
`513`	`513`	`// If the page we arrive on has link to a given lint, we scroll to it.`
`514`	`514`	`function scrollToLintByURL() {`
`515`		`- const lintId = window.location.hash.substring(2);`
	`515`	`+ const lintId = window.location.hash.substring(1);`
`516`	`516`	`if (lintId.length > 0) {`
`517`	`517`	`scrollToLint(lintId);`
`518`	`518`	`}`