Description
If merge A and merge B both try to increase the version from 10 to 11, git will helpfully merge both of them, resulting in the version 11 having both changes. If a nightly is released in the time between A and B are merged, then both will claim to have the save version, but with different features.
This almost happened with #94009 and #94150, but was prevented by manual noticing and intervension, which is not ideal.
We should figure out a way such that if 2 commits both attempt to merge the same increments, git will raise this as a merge conflict, so this situation wont occor again.
A way to do this would be to store in a comment the logical "latest feature"
Eg: PR Foo
-// Latest Feature: Initial release
-const FORMAT_VERSION = 1;
+// Latest Feature: Foo
+const FORMAT_VERSION = 2;
PR Bar:
-// Latest Feature: Initial release
-const FORMAT_VERSION = 1;
+// Latest Feature: Bar
+const FORMAT_VERSION = 2;
If Foo is merged, when Bar is attempted to be merged, the following conflict will occor
<<<<<<< HEAD
// Latest Feature: Foo
=======
// Latest Feature: Bar
>>>>>>> bar
const FORMAT_VERSION = 2;
This could work, but will have a problem if two features are given the same name, and then we're back to where we were. If someone knows some git-trickery to get around that, that would be great, but if not, I still thing doing this (or something to this effect) would be worthwhile.
@rustbot modify labels: +T-rustdoc +A-rustdoc-json