diff options
| author | 2014-03-04 20:51:27 +0100 | |
|---|---|---|
| committer | 2014-03-04 20:51:27 +0100 | |
| commit | c88fa62dd8728db8f58f599808f2d2be49c78f64 (patch) | |
| tree | 70b2196100b7568d8f9133af82d4a71515439c6d /p/api/greader.php | |
| parent | b5df82c4c778d4cea8a5ef41bfb439f30fb6d8f3 (diff) | |
API: better test for server compatibility
https://github.com/marienfressinaud/FreshRSS/issues/443
Diffstat (limited to 'p/api/greader.php')
| -rw-r--r-- | p/api/greader.php | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/p/api/greader.php b/p/api/greader.php index ab2a210a2..adc400790 100644 --- a/p/api/greader.php +++ b/p/api/greader.php @@ -110,9 +110,13 @@ function serviceUnavailable() { function checkCompatibility() { logMe("checkCompatibility()\n"); header('Content-Type: text/plain; charset=UTF-8'); - $ok = true; - $ok &= function_exists('getallheaders'); - echo $ok ? 'PASS' : 'FAIL'; + if (!function_exists('getallheaders')) { + die('FAIL getallheaders!'); + } + if (PHP_INT_SIZE < 8 && !function_exists('gmp_init')) { + die('FAIL 64-bit or GMP extension!'); + } + echo 'PASS'; exit(); } |
