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