From c2243b78c7d532ea835c62d83b686a4cc2fb01bf Mon Sep 17 00:00:00 2001
From: Marius van Witzenburg <info@mariusvw.com>
Date: Wed, 16 Sep 2015 14:35:47 +0200
Subject: [PATCH] Use empty instead of isset, due REMOTE_USER should not be
empty.
---
inc/html.php | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/inc/html.php b/inc/html.php
index 212d9507a..b61a5654b 100644
--- a/inc/html.php
+++ b/inc/html.php
@@ -74,7 +74,7 @@ function html_login(){
function html_denied() {
print p_locale_xhtml('denied');
- if(!isset($_SERVER['REMOTE_USER'])){
+ if(empty($_SERVER['REMOTE_USER'])){
html_login();
}
}
--
GitLab