diff --git a/include/pidfile.php b/include/pidfile.php new file mode 100644 index 0000000000..47df8d1f46 --- /dev/null +++ b/include/pidfile.php @@ -0,0 +1,32 @@ +_file = "$dir/$name.pid"; + + if (file_exists($this->_file)) { + $pid = trim(file_get_contents($this->_file)); + if (posix_kill($pid, 0)) { + $this->_running = true; + } + } + + if (! $this->_running) { + $pid = getmypid(); + file_put_contents($this->_file, $pid); + } + } + + public function __destruct() { + if ((! $this->_running) && file_exists($this->_file)) { + unlink($this->_file); + } + } + + public function is_already_running() { + return $this->_running; + } +} +?>