0) { $value = db_fetch_result($result, 0, "value"); $type_name = db_fetch_result($result, 0, "type_name"); if ($type_name == "bool") { return $value == "true"; } else if ($type_name == "integer") { return sprintf("%d", $value); } else { return $value; } } else { die("Fatal error, unknown preferences key: $pref_name"); } } ?>