Merging PRs while builds are running doesn't seem to queue another job

Assume a build is running after a merged PR in bootstrap. The job starts, waits out the 10 minutes, and starts building. AFAICT, when another PR is merged during this xbbs build, that PR will not trigger a build for it to be queued.