Merge branch 'develop' into improvement/ping-performance

diff --cc boot.php
Simple merge

diff --cc include/dbstructure.php
Simple merge

diff --cc include/session.php
index 5cf4bcc9cffaf30a95320c44ef8f940448e8e22a,c69a4023176889f441cc27023043e7e2dc67b33d..763b05f48166babb5d8eaf28976a22de68e8f587
--- 1/include/session.php
--- 2/include/session.php
+++ b/include/session.php
@@@ -23,22 -36,10 +36,23 @@@ function ref_session_read($id) 
        } else {
                logger("no data for session $id", LOGGER_TRACE);
        }
+ 
        return '';
- }}
+ }
  
 +/**
 + * @brief Standard PHP session write callback
 + *
 + * This callback updates the DB-stored session data and/or the expiration depending
 + * on the case. Uses the $session_expire global for existing session, 5 minutes
 + * for newly created session.
 + *
 + * @global bool $session_exists Whether a session with the given id already exists
 + * @global int $session_expire Session expiration delay in seconds
 + * @param string $id Session ID with format: [a-z0-9]{26}
 + * @param string $data Serialized session data
 + * @return boolean Returns false if parameters are missing, true otherwise
 + */
  function ref_session_write($id, $data) {
        global $session_exists, $session_expire;