Unfortunately, in most cases the answer is probably yes. (You should revert the revert commit.)
I say "unfortunately" because in retrospect the two reverts together add unnecessary (and possibly confusing) commits to your history. Here are two possible alternatives to this:
- Reset the branch and force push it out. This results in a cleaner history, but for a shared remote branch such as
develop, conditions have to be nearly perfect to even consider doing this outside of emergencies. (By nearly perfect I mean: no new commits on the branch, very little time has passed since the bad commits were added and/or it's unlikely others have branched off of it yet, etc.) - You could re-create the branch that was originally merged in, and then rebase it onto itself from the starting commit using
git rebase --no-ff [merge-base-commit]. This will force the rebase to rewrite the commits so they can be re-merged. I might choose this if new commits were added to that previous branch and now it is ready to be brought in again.
But in general, most of the time, on a shared remote develop, it's probably going to be revert the revert.