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.

Voor het installeren van scripts heb je een extensie nodig, zoals Tampermonkey, Greasemonkey of Violentmonkey.

Voor het installeren van scripts heb je een extensie nodig, zoals Tampermonkey of Violentmonkey.

Voor het installeren van scripts heb je een extensie nodig, zoals Tampermonkey of Violentmonkey.

Voor het installeren van scripts heb je een extensie nodig, zoals Tampermonkey of Userscripts.

Voor het installeren van scripts heb je een extensie nodig, zoals {tampermonkey_link:Tampermonkey}.

Voor het installeren van scripts heb je een gebruikersscriptbeheerder nodig.

(Ik heb al een user script manager, laat me het downloaden!)

Voor het installeren van gebruikersstijlen heb je een extensie nodig, zoals {stylus_link:Stylus}.

Voor het installeren van gebruikersstijlen heb je een extensie nodig, zoals {stylus_link:Stylus}.

Voor het installeren van gebruikersstijlen heb je een extensie nodig, zoals {stylus_link:Stylus}.

Voor het installeren van gebruikersstijlen heb je een gebruikersstijlbeheerder nodig.

Voor het installeren van gebruikersstijlen heb je een gebruikersstijlbeheerder nodig.

Voor het installeren van gebruikersstijlen heb je een gebruikersstijlbeheerder nodig.

(Ik heb al een beheerder - laat me doorgaan met de installatie!)

// ==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';