Closed phiros closed 9 years ago
I finally pulled in the changes from master (took me quite some time; master and this branch diverged quite a bit).
@knownasilya Could we merge this PR even though I decreased the coverage? I'd argue that core is a prototype right now so I think it is justified to do so (I expect the code base to stay a little bit volatile for quite some time; we can increase the coverage latter when we worked out how core should work in detail)
BTW: just noticed that there was something wrong with my git config.
All of my commits are authored by 'Travis CI'. Don't know why.
Anyway, I discovered that it is quite hard to amend my commits after I
merged my branch with master. Any idea on how to fix this?
(I already tried the usual git rebase -i c5d3af4^
and marking all my commits
for amending; this fails as soon as I reach the merge commit)
Looks like http://schacon.github.io/git/git-filter-branch.html would be the solution, and just change the author of all the commits in your PR branch, then force push.
@knownasilya thanks for the hint (didn't know this command existed). I should really find some time to read the git pro book at some point in the near future...
This PR can unfortunately not be merged automatically with master since this branch diverged quite a bit from master (@knownasilya I simply didn't notice that you pushed directly to master until yesterday). I will rebase this PR on master in the next few days before I continue working on this.
What currently works: