diff options
Diffstat (limited to 'javascript')
-rw-r--r-- | javascript/ui.js | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/javascript/ui.js b/javascript/ui.js index 611b70d1..ed9673d6 100644 --- a/javascript/ui.js +++ b/javascript/ui.js @@ -395,7 +395,16 @@ function update_token_counter(button_id) { function restart_reload(){ document.body.innerHTML='<h1 style="font-family:monospace;margin-top:20%;color:lightgray;text-align:center;">Reloading...</h1>'; - setTimeout(function(){location.reload()},2000) + + var requestPing = function(){ + requestGet("./internal/ping", {}, function(data){ + location.reload(); + }, function(){ + setTimeout(requestPing, 500); + }) + } + + setTimeout(requestPing, 2000); return [] } |