I did the latter. But somehow along the way the commits made their way into there... what I can do from now on is just try to rewrite history *before* pushing to github and see if something is redundant. And of course, go on a commit diet. Thanks for the tip Peter, and again, I apologize for the mess.