// ==UserScript==
// @name          MysqlDocFix
// @namespace     http://www.cyberpomo.com/
// @description   Korrigera fonter i Mysql-dokumentationen
// @include       http://dev.mysql.com/*
// ==/UserScript==

function addGlobalStyle(css) {
    var head, style;
    head = document.getElementsByTagName('head')[0];
    if (!head) { return; }
    style = document.createElement('style');
    style.type = 'text/css';
    style.innerHTML = css;
    head.appendChild(style);
}

addGlobalStyle("p {font-size: 125% !important;}");