// Fix pull request comments for outdated diffs:
// (via https://gist.github.com/aseemk/5274164)

var DIFF_COMMENT_REGEX = /\/files(\/\w+)?#(r(\w+))/;
    // new style: ...pull/123/files/abcdef1234567890#r12345678
    // old style: ...pull/123/files#r12345678

var diffCommentMatch = location.href.match(DIFF_COMMENT_REGEX);
var diffCommentId = diffCommentMatch && diffCommentMatch[2];
var diffCommentNum = diffCommentMatch && diffCommentMatch[3];

if (diffCommentId && !document.getElementById(diffCommentId)) {
    // TODO can we use history.pushState() instead, to be faster?
    // need to figure out how to get GitHub to respond to the change.
    // $(window).trigger('popstate') doesn't seem to do the trick.
    location.replace(location.href.replace(
        DIFF_COMMENT_REGEX, '#discussion_r' + diffCommentNum));
}