Accélerer sensiblement le mirror sur des appels successifs : gitea renvoie que le projet a été modifié (donc sa date de dernière modification change) lorsqu’un tag est posé par exemple, et pas uniquement sur un commit.

De ce fait, le fichier `index` n’est pas toujours modifié et donc sa date ne change pas dans ce cas, et à chaque exécution un git pull est alors fait, même s’il n’y a pas de changement.
On s’appuie dans ce cas sur la date du dernier `git pull` avec le fichier FETCH_HEAD : on l’utilise s’il existe, sinon on se rabat sur `index` (s’il y a juste eu un clone, et aucun changement depuis).

mirror.php

@@ -1,4 +1,4 @@
-#!/usr/bin/php
+#!/usr/bin/env php
 <?php
 
 // quelques constantes pour faire marcher les fonctions copie-colle de SPIP ou du plugin debardeur
@@ -54,28 +54,36 @@ foreach ($url_orgs as $url_org) {
 		if ($repo['empty']) {
 			$empty[] = $url;
 			echo " => Vide\n";
-		}
-		else {
-			$gitindex = "$dir/.git/index";
-			if (!is_dir($dir)
-			  or !file_exists($gitindex)
-			  or !$t = filemtime($gitindex)
-			  or $t < $last_modified) {
+		} else {
+			$git_last_change = "$dir/.git/index";
+			$git_last_pull = "$dir/.git/FETCH_HEAD";
+			if (
+				!is_dir($dir)
+				or !file_exists($git_last_change)
+				or (
+					file_exists($git_last_pull) 
+					and $t = filemtime($git_last_pull)
+					and $t < $last_modified
+				)
+				or (
+					!file_exists($git_last_pull)
+					and $t = filemtime($git_last_change)
+					and $t < $last_modified
+				)
+			) {
 				$updated[] = $url;
 				if (file_exists("$dir/.ignore")) {
 					$errors[] = $url;
-				}
-				else {
+				} else {
 					$cmd = "checkout -bmaster $url $dir";
 					echo "\n$cmd\n";
 					passthru($cmd);
 					echo "\n";
-					if (!file_exists($gitindex)) {
+					if (!file_exists($git_last_pull)) {
 						$errors[] = $url;
 					}
 				}
-			}
-			else {
+			} else {
 				echo " => OK\n";
 			}
 		}