+ <script type="text/javascript">
+ <?php
+ require 'lib/jshrink/Minifier.php';
+
+ global $pluginhost;
+
+ foreach ($pluginhost->get_plugins() as $n => $p) {
+ if (method_exists($p, "get_prefs_js")) {
+ echo JShrink\Minifier::minify($p->get_prefs_js());
+ }
+ }
+
+ print get_minified_js(array("functions", "deprecated", "prefs", "PrefFeedTree", "PrefFilterTree", "PrefLabelTree"));
+
+ init_js_translations();
+ ?>
+ </script>