Closed arximboldi closed 8 years ago
The build server cannot build this PR because the author is not whitelisted. A meatbag will have to look at it.
This is an automated message.
Oh shit, I missed that you merged this, I am going to remake this on top
of current devel
.
"R. Martinho Fernandes" notifications@github.com writes:
Merged #65.
You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub: https://github.com/rmartinho/nonius/pull/65#event-775008705
Done, again :-)
"R. Martinho Fernandes" notifications@github.com writes:
Merged #65.
You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub: https://github.com/rmartinho/nonius/pull/65#event-775008705
No worries. I wanted to make a beta release from the current PRs and I kinda messed up with this one because I thought I had gone over it before, which I now doubt I did :D (I even got the docs wrong :S). I also realised I will want to deal with deprecation and backwards-compatibility (#68) before this gets shipped.
For now I reverted this :/ GitHub doesn't seem to have a way to mark a PR as unmerged, though.
Doubles are reserved everywhere, no exceptions.
Yeah, I see that the pull request did also not updated with my latest push to this branch. I am going to re-open the PR so we can discuss further improvements there.
Addresses #10