Redirect PostgreSQL.org docs to current version

Very useful when coming from elsewhere and ending up with docs some random ancient version.

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==
// @namespace https://kludge.guru/
// @name Redirect PostgreSQL.org docs to current version
// @description Very useful when coming from elsewhere and ending up with docs some random ancient version.
// @match https://www.postgresql.org/docs/*
// @version          1.0
// ==/UserScript==

function maybeRedirect() {

  if (!document.referrer || document.referrer.indexOf('https://www.postgresql.org') === 0) { return; }

  const { pathname } = document.location;
  const match = pathname.match(/^\/docs\/[0-9\.]+\/(.*)$/);
  if (!match) { return; }

  const url = `/docs/current/${match[1]}`;
  const a = document.querySelector(`a[href="${url}"]`);
  if (!a) { return; }

  location.replace(url);

}

maybeRedirect();