diff options
author | Tobias Bell <[email protected]> | 2018-06-08 22:07:30 +0200 |
---|---|---|
committer | Tobias Bell <[email protected]> | 2018-06-08 22:07:30 +0200 |
commit | af3663edec48f252f510f66f663e1af323cdfa0f (patch) | |
tree | 4884c570d1d58b0e6786ffbdc5413ed8f335e3cd | |
parent | f5302247c6eecba217f35173b3f038cc828a7402 (diff) |
Don't bail out if git gc removed refs
-rw-r--r-- | include/version.php | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/include/version.php b/include/version.php index 1d7567bb1..2cf7b1ded 100644 --- a/include/version.php +++ b/include/version.php @@ -14,6 +14,8 @@ if (preg_match("/^ref: (.*)/", $head, $matches)) { $ref = $matches[1]; + if (!file_exists("$root_dir/.git/$ref")) + return VERSION_STATIC; $suffix = substr(trim(file_get_contents("$root_dir/.git/$ref")), 0, 7); $timestamp = filemtime("$root_dir/.git/$ref"); |