search

devhub-tud / devhub

DevHub is a software system designed to give students a simple practical introduction into modern software development.
15 stars 8 forks source link

Merging pull request failed for group #443

Closed TimvdLippe closed 7 years ago

TimvdLippe commented 7 years ago

Using the pull request UI of github, one pull request was not merged into master.

The initial try was https://devhub.ewi.tudelft.nl/courses/ti1706/1617/groups/22/pull/10/ while I tried https://devhub.ewi.tudelft.nl/courses/ti1706/1617/groups/22/pull/11/ The pull request does get closed, but the commits are not pushed onto the master branch. A manual git merge assignment/assignment_2.11 locally and then git push origin master was working as planned.

jwgmeligmeyling commented 7 years ago

Did you do some git surgery on that repository prior to merging? Such as repository rewinding?

TimvdLippe commented 7 years ago

I did not. I did a git pull origin master, that was up-to-date. The branch was also up-to-date. Then I merged without issues. I did not execute any other commit nor any resets or anything

jwgmeligmeyling commented 7 years ago

I forgot to deploy https://github.com/devhub-tud/git-server/pull/91 , let's see whether its fixed now.

jwgmeligmeyling commented 7 years ago

I suppose its fixed now.