Why does `import Mathlib` break `include_str`?

Stream: general

[Greg Shuflin]

I'm using the include_str directive in a project. When I add the line import Mathlib, with no other code, I suddenly get compiler errors on the include_str line saying there are two interpetations of the line, both with the same text from the same file. I'm not sure why this is happening - presumably Mathlib has its own version of include_str that conflicts with the built-in one, but is import Mathlib supposed to include anything new in the current scope at all?

[Ruben Van de Velde]

Yes, absolutely to the last question

[Ruben Van de Velde]

The copy in mathlib was removed in #19828, though