// ==UserScript==
// @name           Symbolics
// @namespace      x
// @include        http://symbolics.nl/*
// ==/UserScript==

function stretchit() {
  var ysmin=543;
  var diff=317;
  var cont=this.document.getElementById("contents");
  var stre=this.document.getElementById("stretchy");
  var yc=cont.scrollHeight;
  var ys=stre.scrollHeight;
  yc>ysmin+diff?stre.height=yc-diff:stre.height=ysmin;
}