Reload GitHub Pull Request Diff page to ignore whitespace

Reloads the GitHub Pull Request Diff page, adjusting the URL to have the diffs ignore whitespace.

You will need to install an extension such as Tampermonkey, Greasemonkey or Violentmonkey to install this script.

You will need to install an extension such as Tampermonkey or Violentmonkey to install this script.

You will need to install an extension such as Tampermonkey or Violentmonkey to install this script.

You will need to install an extension such as Tampermonkey or Userscripts to install this script.

You will need to install an extension such as Tampermonkey to install this script.

You will need to install a user script manager extension to install this script.

(I already have a user script manager, let me install it!)

You will need to install an extension such as Stylus to install this style.

You will need to install an extension such as Stylus to install this style.

You will need to install an extension such as Stylus to install this style.

You will need to install a user style manager extension to install this style.

You will need to install a user style manager extension to install this style.

You will need to install a user style manager extension to install this style.

(I already have a user style manager, let me install it!)

// ==UserScript==
// @name        Reload GitHub Pull Request Diff page to ignore whitespace
// @namespace   https://bitbucket.org/deadlydog/greasemonkeyscripts
// @description Reloads the GitHub Pull Request Diff page, adjusting the URL to have the diffs ignore whitespace.
// @include     https://github.com/*/pull/*/files
// @exclude     https://github.com/*/pull/*/files?w=1
// @grant       none
// @version     1.1
// ==/UserScript==

// Wipe out the head and body contents so that we don't wait for them to load before doing the redirect.
document.head.innerHTML='';
document.body.innerHTML='';

// Redirect to the URL we are at, with the special modifier attached that signals to ignore whitespace in the diffs.
window.location.href=window.location.href + '?w=1';