import Foo.«英語» doesn't work

[lovettchris]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

It should work according to the documentation on lexical structure

which says an escaped identifier can contain anything except «»\r\n\t

escaped_ident_part: "«" [^«»\r\n\t]* "»"

Steps to Reproduce

Load the attached lean package into vscode:

utf8test.tar.gz

Expected behavior:

It should work, and the Hello function should evaluate and print Hello, 英語!

Actual behavior:

`leanpkg print-paths` failed:

stderr:
configuring Foo 0.1
no such file or directory (error code: 2)
  file: .\Foo\

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version, please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.