wip #5220 @1

diff --git a/inc/ws/Controlleur/class.ws.maintenance.php b/inc/ws/Controlleur/class.ws.maintenance.php
index a6b9c95460a0f04513d02e6dded0d4bf96ef2f93..b1bcd35893dd0d89a1f5157e3e4584164609cbaa 100644 (file)
--- a/inc/ws/Controlleur/class.ws.maintenance.php
+++ b/inc/ws/Controlleur/class.ws.maintenance.php
@@ -1850,8 +1850,24 @@ class wsMaintenance
     {
         $originalConnectionTimeout = ini_get('default_socket_timeout');
         ini_set('default_socket_timeout', 5);
+        $cache = WS_CACHE . '/farmpings';
+        $servers = wsDocument::getFarmServers();
         $pings = [];
-        foreach (wsDocument::getFarmServers() as $id => $farmer) {
+        if (file_exists($cache)) {
+            $cached = json_decode(file_get_contents($cache));
+            if (count($cached) === count($servers)) {
+                $pings = $cached;
+            }
+        }
+
+        foreach ($servers as $id => $farmer) {
+            if (isset($pings[$id]) || !$pings[$id]) {
+                // If ping failed recently, we wait a bit before trying again.
+                if (rand(0, 9) === 5) {
+                    continue;
+                }
+                break;
+            }
             echo '<h2>' . $farmer['host'] . ' (' . $id . ')</h2>';
             $cl = new CubeIT_CommandLine('/usr/local/fluidbook_processfarm/bin/ping');
             $cl->setSSH($farmer['host'], 'fluidbookfarmer', '', $farmer['port'] ?? 22, '/home/extranet/.ssh/id_rsa');
@@ -1861,7 +1877,7 @@ class wsMaintenance
 
             $pings[$id] = $ok;
         }
-        file_put_contents(WS_CACHE . '/farmpings', json_encode($pings));
+        file_put_contents($cache, json_encode($pings));
         ini_set('default_socket_timeout', $originalConnectionTimeout);
     }
 
@@ -1889,7 +1905,7 @@ class wsMaintenance
             ['svg', '150', true, false, 'html'],
             ['svg', '300', true, false, 'html'],
             ['svg', '150', true, true, 'html'],
-            ['svg', '200', true, true, 'html'],
+            ['svg', '300', true, true, 'html'],
         ];
 
         foreach ($files as $file) {