Zulip Chat Archive
Stream: new members
Topic: Error for rebuilting?
天语遥Vera (Jan 25 2025 at 19:28):
When I'am loading the forlder " Mathematics_in_Lean", there's an error that "Imports are out of date and must be rebuilt; use the "Restart File" command in your editor." I wonder what does this mean? And how to improve it please?
Last updated: May 02 2025 at 03:31 UTC