[web] Jump to error on files with double slash GitOrigin-RevId: eec2ac6ba7a34d32f757f5e3a088e92d0d494422
@@ -167,6 +167,7 @@ function buildURL(file, pdfDownloadDomain) {
}
function normalizeFilePath(path, rootDocDirname) {
+ path = path.replace(/\/\//g, '/')
path = path.replace(
/^.*\/compiles\/[0-9a-f]{24}(-[0-9a-f]{24})?\/(\.\/)?/,
''