Open jgvictores opened 5 years ago
Blocked by #55
Update: I tried to do a local merge between develop and master and worked, should i make a push to the remote?
The master branch only differs in two merge commits from develop, so you could as well either delete it and create anew or force push from current develop.
From master: "This branch is 2 commits ahead, 416 commits behind develop."
That's more than two commits hahaha
Nope, that's exactly two commits if your base branch is develop. Those commits are meaningless in this comparison since both come from develop anyway, thus merging develop into master means you can start a new master branch on top of develop with little or no harm (okay, you are rewriting the commit history on a shared repo, but IMO it can be assumed given how the network graph for master branch looks like).
Ok, now I understand your point, and yeah looks fine to me to delete the master branch and create a new one in develop, that can help reduce the mess in the network :D
Done
Today, develop
has been merged into master
because of https://github.com/roboticslab-uc3m/questions-and-answers/issues/88.
clean branches: cannot be merged automatically