- $page_header_php = true;
-
- if (!isset($prefs_php))
- include ("../functions/prefs.php");
- if (!isset($i18n_php))
- include ("../functions/i18n.php");
- if (!isset($plugin_php))
- include ("../functions/plugin.php");
-
- // Check to see if gettext is installed
- set_up_language(getPref($data_dir, $username, "language"));
-
- // This is done to ensure that the character set is correct.
- if ($default_charset != "")
- header ("Content-Type: text/html; charset=$default_charset");