Resolve extension number on merge

[pwinckles]

Perhaps the merge policy should be updated to specify that an extension's number should be resolved immediately prior to merging. For example, PR #20 was just merged, creating extension 0006-flat-direct-storage-layout. Now there is a gap in the merged extensions. This gap will be filled if all of the existing PR merged, but will leave holes if they are not.

So, I guess the question is, are we okay with holes? If so, extensions claiming the next available number when their PR is submitted is fine. If not, we should update the extension number immediately before merging.

[zimeon]

I think we could quickly rewrite history and change 0006-flat-direct-storage-layout to 0002-flat-direct-storage-layout then adopt the policy that @pwinckles propses -- I think it would be best not to create holes

[awoods]

+1 to "no holes" and changing 0006-flat-direct-storage-layout to 0002-flat-direct-storage-layout.

[rosy1280]

@pwinckles we discussed adding language to the merge policy that says something like: extensions should remain nnnn and then before merge an editor will update the PR to include the appropriate extension number. thoughts?

[pwinckles]

@pwinckles we discussed adding language to the merge policy that says something like: extensions should remain nnnn and then before merge an editor will update the PR to include the appropriate extension number. thoughts?

Yep, that sounds good to me