This message was deleted.
# report-bugss
Slackbot
07/30/2023, 11:07 PMThis message was deleted.
p
Pranathi Peri
07/31/2023, 2:21 PMThanks for the note! We'll look into it 🙂
d
David Bradford
07/31/2023, 2:24 PMAre the commits in the git history in the expected order?
🙏 1
David Bradford
07/31/2023, 2:26 PMWe have occasionally been seeing some strange behavior from github, where it takes a surprisingly long time to detect that the PR has been merged. It seems to be really inconsistent. And if it is just the timing of the github merge events that you are seeing, then it is likely related.
David Bradford
07/31/2023, 2:27 PMI'm currently investigating some other approaches to how we handle merges that I don't think have this problem.