db-prefs: use user_error

diff --git a/include/db-prefs.php b/include/db-prefs.php
index 125f1caaa44bfe6413e29f30c8be4bbdcbc5e06e..8336b0cfee5a0734ca9c9d36b57f22ce2dcba442 100644 (file)
--- a/include/db-prefs.php
+++ b/include/db-prefs.php
@@ -97,7 +97,7 @@
 
                } else {
                        if ($die_on_error) {
 
                } else {
                        if ($die_on_error) {

-                               die("Fatal error, unknown preferences key: $pref_name");
+                               user_error("Fatal error, unknown preferences key: $pref_name", E_USER_ERROR);

                        } else {
                                return null;
                        }
                        } else {
                                return null;
                        }