Remove unused javascript

This is from the old version of the website, and hasn't been used for
quite some time.
This commit is contained in:
Magnus Hagander
2020-09-12 12:21:12 +02:00
parent 087be8458b
commit c40cc5e223

View File

@ -1,27 +0,0 @@
function display_default_font_size(id)
{
var x = document.getElementById(id);
if (x.currentStyle)
var y = x.currentStyle['fontSize'];
else if (window.getComputedStyle)
var y = document.defaultView.getComputedStyle(x,null).getPropertyValue('font-size');
return y;
}
document.write('<pre id="monotest" style="display: none;">&nbsp;</pre>');
document.write('<p id="paratest" style="display: none;">&nbsp;</p>');
var monoSize = parseInt(display_default_font_size("monotest"));
var propSize = parseInt(display_default_font_size("paratest"));
var newMonoSize = propSize / monoSize;
if (newMonoSize != 1)
{
document.write('<style type="text/css" media="screen">'
+ '#docContainer tt, #docContainer pre, #docContainer code'
+ '{font-size: ' + newMonoSize.toFixed(1) + 'em;}\n'
/* prevent embedded code tags from changing font size */
+ '#docContainer code code'
+ '{font-size: 1em;}</style>\n');
}