Fix check_links script to deal with new doc ids

marijnh · marijnh · commit 932bb072029c · 2014-07-23T16:10:40.000+02:00
diff --git a/bin/check_links.js b/bin/check_links.js
@@ -20,7 +20,7 @@ for (var file in files) {
     var target = files[m[1]];
     if (!target)
       error(file, "Unknown target file: " + m[0]);
-    else if (target.indexOf("[[" + m[3] + "]]") == -1)
+    else if (m[3] != m[1].slice(3) && target.indexOf("[[" + m[3] + "]]") == -1)
       error(file, "Non-existing anchor: " + m[0]);
   }
 }

Original file line number	Diff line number	Diff line change
`@@ -20,7 +20,7 @@ for (var file in files) {`
`20`	`20`	`var target = files[m[1]];`
`21`	`21`	`if (!target)`
`22`	`22`	`error(file, "Unknown target file: " + m[0]);`
`23`		`- else if (target.indexOf("[[" + m[3] + "]]") == -1)`
	`23`	`+ else if (m[3] != m[1].slice(3) && target.indexOf("[[" + m[3] + "]]") == -1)`
`24`	`24`	`error(file, "Non-existing anchor: " + m[0]);`
`25`	`25`	`}`
`26`	`26`	`}`