Remove unused javascript
authorMagnus Hagander <magnus@hagander.net>
Sat, 12 Sep 2020 10:21:12 +0000 (12:21 +0200)
committerMagnus Hagander <magnus@hagander.net>
Sat, 12 Sep 2020 10:48:45 +0000 (12:48 +0200)
This is from the old version of the website, and hasn't been used for
quite some time.

media/js/monospacefix.js [deleted file]

diff --git a/media/js/monospacefix.js b/media/js/monospacefix.js
deleted file mode 100644 (file)
index 205e814..0000000
+++ /dev/null
@@ -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');
-}
-