import files with spaces

Stream: new members

[Pedro Minicz]

Suppose I have a Lean file with spaces on its name, say Hello World.lean, is it possible for me to import it from another file? I tried import .Hello World, import .Hello\ World and import ".Hello World", none of which worked, so I suspect it is impossible.

[Reid Barton]

This seems to work:

import .«Hello World»

but also maybe just don't do that?

[Pedro Minicz]

Thanks!