From 6ba3c8bfca510e8afbee7f6422a0c395d83d3636 Mon Sep 17 00:00:00 2001
From: Christoph Reiter <reiter.christoph@gmail.com>
Date: Sun, 23 Jan 2022 10:53:15 +0100
Subject: [PATCH] fetch: wait 5 seconds after we get triggered via the api

it seems sometimes we update things at github, but it takes some time
until our server sees the new version, so wait a bit.
---
 app/fetch.py | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/app/fetch.py b/app/fetch.py
index d3775f0..4bc7831 100644
--- a/app/fetch.py
+++ b/app/fetch.py
@@ -395,3 +395,5 @@ async def update_loop() -> None:
                 traceback.print_exc(file=sys.stdout)
         print("Waiting for next update")
         await wait_for_update()
+        # XXX: it seems some updates don't propagate right away, so wait a bit
+        await asyncio.sleep(5)