phppgadmin/phppgadmin — pull request #6 by rjuju (2012-08-17 09:05:17+00:00)
Title: Fix previous patch issue : when no value for theme in config file

Before previous fix, the theme "default" was always used whatever the value in config file. As it now uses the one in config file, there was an issue if no value for theme is present in config file.

Sorry for double push request.