Add new variable "server_version_num", which is almost the same as

"server_version" but uses the handy PG_VERSION_NUM which allows apps to
do things like if ($version >= 80200) without having to parse apart the
value of server_version themselves.

Greg Sabino Mullane greg@turnstep.com