Error message when name in import starts with digit

Stream: lean4

[Floris van Doorn]

When writing import Mathlib.2X.Test, then I get two errors when I don't have Mathlib fully compiled.

Imports are out of date and must be rebuilt; use the "Restart File" command in your editor.
unexpected token; expected identifier

The import statement is interpreted as import Mathlib.
If I restart the file, all of Mathlib is imported/rebuilt.
Can we get an error if the token after an import is . (perhaps without whitespace)?

[Mac Malone]

@Floris van Doorn I believe this is lean4#2999, which Eric fixed in the recently merged lean4#2994.