Closed NogginBops closed 1 month ago
I think I might have messed up the git stuff as I think some of these commits are part of #534. Not sure if I can fix this in any good ways.
I think this is because #534 was squash-merged.
In other words, an equivalent commit was added to the main
branch, so this PR is compatible, but the commits of #534 themselves are not on main - so they are shown in changes.
One way to fix this is to rebase the more-kind-changes
branch onto the main branch.
Rebase would make the current main
- the origin of the changes, as if you started from scratch and cherry-picked every commit of this PR in the same order, discarding the now no-op commits (because they were already merged into main).
Though rebase might be messy in this case.
It might be easier to reset --hard
the more-kind-changes
branch onto the main branch, and manually cherry-pick the only relevant commits from the remote version of this branch.
Either way, you'd need to push --force
(or push --force-with-lease
) to fix how it looks on GitHub.
Before forcing new (alternative) history onto GitHub, I recommend that you diff the remote and the local (rebased) states of the more-kind-changes
branch to make sure there aren't any changes you were unaware of.
git cherry-pick
in the specific commits that where missing in #534 into a new branch based on main
.There are 3 changes in gl.xml between the last 2 PRs.
Well, the first 2 look reasonable (though it's weird why it was like that in this PR), but the third one is a kind="Range[0; x]"
=> kind="CheckedInt32"
change.
Will fix!
This PR fixes the last stuff that was left in in #534. Basically this PR replaces and removes the last
CheckedFloat
andCheckedInt32
kinds (as well a few others kinds that where leftovers and never described formally).I thought I had fixed these things but it turned out that I had some +1 year old commits in this branch that I never opened a PR for.
cc @SunSerega