Merge pull request #2220 from FreshRSS/dev1.13.1

FreshRSS 1.13.1

1 files changed, 4 insertions, 1 deletions

diff --git a/constants.php b/constants.php
index 1f498b153..8a49d7c01 100644
--- a/constants.php
+++ b/constants.php
@@ -2,7 +2,7 @@
 //NB: Do not edit; use ./constants.local.php instead.
 
 //<Not customisable>
-define('FRESHRSS_VERSION', '1.13.0');
+define('FRESHRSS_VERSION', '1.13.1');
 define('FRESHRSS_WEBSITE', 'https://freshrss.org');
 define('FRESHRSS_WIKI', 'https://freshrss.github.io/FreshRSS/');
 
@@ -32,6 +32,9 @@ safe_define('FRESHRSS_USERAGENT', 'FreshRSS/' . FRESHRSS_VERSION . ' (' . PHP_OS
 // PHP text output compression http://php.net/ob_gzhandler (better to do it at Web server level)
 safe_define('PHP_COMPRESSION', false);
 
+// For cases when syslog is not available
+safe_define('COPY_SYSLOG_TO_STDERR', isset($_SERVER['COPY_SYSLOG_TO_STDERR']) ? filter_var($_SERVER['COPY_SYSLOG_TO_STDERR'], FILTER_VALIDATE_BOOLEAN) : false);
+
 // Maximum log file size in Bytes, before it will be divided by two
 safe_define('MAX_LOG_SIZE', 1048576);