I think there have been some delays syncing between github and gitbox. I think it depends which origin you are pointing at and which commit is there.
Since both github and gitbox are masters, we can actually push to either one and I would guess there is some checks to make sure commits don't have issues but a pull might be slightly out of date? Kevin Risden On Wed, May 22, 2019 at 5:12 PM Julian Hyde <[email protected]> wrote: > I pushed a commit to the master branch this morning and it was > rejected due to an intervening commit from Laurent. But that > intervening commit did not appear when I did 'git fetch origin'. > > Just now, I was just able to push successfully. In both cases I used > 'git push origin master' from the command line, without the '-f' > (force) flag. > > You can see that both commits generated emails: [1] [3]. Laurent's > intervening commit also generated an email: [2]. > > All, Has anyone else seen this behavior? > > Laurent, What command did you use to commit? > > Julian > > [1] > https://lists.apache.org/thread.html/ac70079b65305a9040bfe2ed0720768343d2f6dc038b9a63c081ff0b@%3Ccommits.calcite.apache.org%3E > > [2] > https://lists.apache.org/thread.html/bddfd2ad8cbe3148820b334b1554fae23d4e05a2b00967b71e5d7191@%3Ccommits.calcite.apache.org%3E > > [3] > https://lists.apache.org/thread.html/335c042be3fbd042f327e9742d45de790d731d8a7f883294dacf9322@%3Ccommits.calcite.apache.org%3E >
