public static function getHTTPStatusCode($header)
  {
    $first_line = strtok($header, "\n");
    
    preg_match("# [0-9]{3}#", $first_line, $match);
    
    if (isset($match[0]))
      return (int)trim($match[0]);
    else
      return null;
  }