Undefined index: HTTP_USER_AGENT in themekey_dummy2user_os()

PHP 5.3
Drupal 7.19
Themekey 7.x-2.3

I am using the system:user_os_simplified rule to load a theme based on mobile browsers [system:user_os_simplified ~ (iPhone|iPad|Android|Blackberry)], I see this notice show up here and there in the log, here's the full message:

Notice: Undefined index: HTTP_USER_AGENT in themekey_dummy2user_os() (line 592 of /public_html/sites/all/modules/themekey/modules/themekey.system.inc).

Looking at the raw access logs for my server, i'm seeing some like this:

63.146.170.241 - - [13/Feb/2013:08:17:36 -0700] "GET /rss/Learn+Peace/19/feed HTTP/1.0" 301 637 "-" "-"

So probably an rss reader or bot or something that does not give an HTTP_USER_AGENT.

Quickly looking at that line, you are passing $_SERVER['HTTP_USER_AGENT'] directly, which in this case is empty, which is throwing the notice (thank you php 5.3), probably need an isset() or !empty() in there. I notice the same for themekey_dummy2user_browser() as well.

Anyway, hardly even rates a minor issue, but something to look into.