settings.php: when printing error, also exit with error code

diff --git a/settings/settings.php b/settings/settings.php
index d45a42376cb3cfe055b62b7dd672b5b927fd91f0..907a9fa0b530804bd776532abf6a3000ba5f2b39 100644 (file)
--- a/settings/settings.php
+++ b/settings/settings.php
@@ -1,4 +1,4 @@
 <?php
 
 echo "ERROR: Scripts must be run from build directory.\n";
-exit;
+exit(1);