noncomputable section breaks section end?

Stream: mathlib4

[Arien Malec]

I have !4#1995 that breaks on invalid 'end', name mismatch; if I comment out noncomputable section, I get a matched begin/end pair (but I have to manually mark everything noncomputable

[Arien Malec]

#mwe

section Foo
noncomputable section
end Foo

[Reid Barton]

noncomputable is a modifier for a section

[Reid Barton]

i.e. it should be noncomputable section Foo / end Foo

[Arien Malec]

Yeah, that was the fix...

[Arien Malec]

I guess mathport renames noncomputable theory to noncomputable section

[Arien Malec]

So

section foo
noncomputable theory
-- blah
end foo

gets translated to

section Foo
noncomputable section
-- blah
end Foo

which breaks.

[Gabriel Ebner]

I think we all expected that noncomputable theory only comes once at the beginning of the file.