galvez

// ==UserScript==
// @name          github-source-font-change.user.js
// @description   Script to change the source code viewer font in GitHub
// @include       https://github.com/*
// @include       http://github.com/*
// @include       http://gist.github.com/*
// ==/UserScript==

function change_font() {
  var pres = document.getElementsByTagName('pre');