Skip to content

Add delay to refresh #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Add delay to refresh #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion TODO
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions server.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down