Warn about inconsistent indentation

[phadej]

This is an effect of using indentOfAtLeast method: any indentation greater than current offset is fine.

That behavior is desirable to parsing multiline field contents, but it is a bit surprising for fields in sections, which we expect to be aligned.

Such insonsistency seems to be always a mistake, and it's easy to fix once a machine points it out.

[phadej]

I had to adjust lexer slightly as BOM and NBSP where throwing source locations a bit off causing cascading indentation warnings.

[ulysses4ever]

I had to adjust lexer slightly as BOM and NBSP where throwing source locations a bit off causing cascading indentation warnings.

This sounds a bit worrying. Have you seen the discussion at #8896? Don't we step on each others toes here?

At the very least, the Lexer change sounds like something that should go into a separate commit.

[phadej]

ping

[Mikolaj]

Thanks a lot. Please kindly set one of the merge labels.

[phadej]

I don't have (and don't want) write permissions to this repository.

[ulysses4ever]

@phadej no worries, I did the labeling. Thanks again! Btw, #8983 has one commit in common with this PR, so maybe it'll need a rebase at some point...

[phadej]

Why isn't this merged? There isn't conflict?

[ulysses4ever]

@mergify rebase

[mergify]

rebase

❌ Pull request can't be updated with latest base branch changes

Mergify needs the author permission to update the base branch of the pull request.
@phadej needs to authorize modification on its head branch.
err-code: 14823

[ulysses4ever]

@phadej on it. Sorry for the delay.

[ulysses4ever]

@mergify refresh

[mergify]

refresh

✅ Pull request refreshed

[Mikolaj]

@mergify refresh

[mergify]

refresh

✅ Pull request refreshed

[Mikolaj]

@mergify rebase

[mergify]

rebase

❌ Pull request can't be updated with latest base branch changes

Mergify needs the author permission to update the base branch of the pull request.
@phadej needs to authorize modification on its head branch.
err-code: 5D20E

[Mikolaj]

Oh dear.

[Mikolaj]

@phadej: we have technical problems; is it fine if I squash the PR when merging? If not, we'd probably need to open a new PR and move it there, but it's work and an indirection.

[ulysses4ever]

@Mikolaj Oleg was very clear about it: he won't allow updates. We'll have to manually copy his branches to our repository and open new PRs using those copies. I am afraid it'll be hard to find volunteers to do this monkey job.

[Mikolaj]

@ulysses4ever: I thought the merge+squash button would be a cheap way out. Wouldn't it work? In any case, @ffaf1 did it in a more principled way, so let's merge his PR.

[ulysses4ever]

@Mikolaj unless I'm missing something, Mergify is completely strangled by not being able to update the branch. Perhaps, you could work around Mergify by clicking GitHub buttons for squash and merge, see the screenshot.

But I find it a bit dangerous to apply both merge approaches (GH and Mergify) on one repository concurrently.

[Mikolaj]

Yes, the button is what I meant. If the button works, then mergify does not cut in. Unless I'm missing something. However, we lose the separate commits.

[ulysses4ever]

Mergify may be surprised that, half-way merging some other PR into master, master suddenly updates. Or the other way around. If you choose exactly the right time for it, I don't see how they (GH and the bot) avoid racing (and these days are rather hot in terms of merging stuff). And then it's the question whether they implemented critical sections correctly. Which I wouldn't bet my money on this.

[Mikolaj]

Huh, I'd hope git would cope fine and then mergify or github trying to merge something absurd would be rebuked by git. OTOH, if they promptly retry with enough reset --hard to convince git, I'm afraid your vision may be right. :[

[ffaf1]

Merged in #9051.