From 85a9cfaecdb208dce20b834bf01a131632ec9935 Mon Sep 17 00:00:00 2001
From: Matt Pass <matt@mattpass.com>
Date: Mon, 27 Apr 2015 16:12:44 +0100
Subject: [PATCH] Set $filemtime if not set, need to use in JSON

---
 lib/file-control-xhr.php | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/lib/file-control-xhr.php b/lib/file-control-xhr.php
index 4b91015..71abdf3 100644
--- a/lib/file-control-xhr.php
+++ b/lib/file-control-xhr.php
@@ -585,6 +585,11 @@ if (!$error && $_GET['action']=="perms") {
 // JSON DATA TO RETURN
 // ===================
 
+// No $filemtime yet? Get it now!
+if (!isset($filemtime)) {
+	$filemtime = $serverType=="Linux" ? filemtime($file) : "1000000";
+}
+
 echo '{
 	"file": {
 		"absPath": "'.$file.'",