diff --git a/TODO b/TODO index c62bb33..59a8bbf 100644 --- a/TODO +++ b/TODO @@ -3,7 +3,7 @@ TODO: Support pull requests from different repositories do something to fetch other remotes if there are pull requests from other remotes. -TODO: Wait after the refresh API is hit before querying for changes on GitHub. +TODO (DONE): Wait after the refresh API is hit before querying for changes on GitHub. It seems like it takes a while (probably ~1min is fine) for mergable pull requests to show up. (Or investigate why this is happening.) Note: the API must return an HTTP response quickly, even though the main refresh action is diff --git a/server.sml b/server.sml index 9421cff..0d40532 100644 --- a/server.sml +++ b/server.sml @@ -145,8 +145,11 @@ fun abort id = else cgi_die 409 ["job ",f," is not stopped: cannot abort"] end +val refresh_delay_duration = Time.fromSeconds 30; + fun refresh () = let + val _ = OS.Process.sleep refresh_delay_duration; val snapshots = get_current_snapshots () val fd = acquire_lock () val () = clear_list "waiting"