First try in VS code

Stream: new members

[PeppoB]

I'm new in the Lean world and I'm trying to follow the 'Mathematics with Lean' with workbooks in VS code. I find the program frequently asks to reload the workbook. Is this expected?

[spamegg]

I'm going through MIL myself and I don't have the issue. But I'm not using workbooks (not sure what that is). I cloned the MIL repository locally.