diff --git a/lib/setup.php b/lib/setup.php
index e15ea3bb15e..84d303e033a 100644
--- a/lib/setup.php
+++ b/lib/setup.php
@@ -408,6 +408,7 @@ global $SCRIPT;
         }
         if (!empty($_SERVER['PATH_TRANSLATED'])) {
             $_SERVER['PATH_TRANSLATED'] = stripslashes($_SERVER['PATH_TRANSLATED']);
+        }
     }
 
 /// neutralise nasty chars in PHP_SELF