Readonly include for elan?

Stream: mathlib4

[Bolton Bailey]

I occasionally accidentally type something in ~/.elan when I am looking through it while editing mathlib, causing the file to rebuild. I am always afraid when I do this that I will not notice and break something, and I never personally want to edit these files anyway.

I propose putting **/.elan/** into a readonly include list in the mathlib workspace settings VSCode settings.json - this would make the files here uneditable unless the user explicitly undoes in in their user settings. This seems to me like a good way to make it clear to someone who might not otherwise realize it that if you navigate to one of these files you have left mathlib.

[Bolton Bailey]

Is there anyone that does edit .elan from the mathlib project in VSCode for whom this would be a bad idea, or any other objections people can think of?

[Bolton Bailey]

Similar question 2: Should we do this for /.lake as well?

[Bolton Bailey]

Similar question 3: Should we add branch protection to master?

[Bolton Bailey]

Bolton Bailey said:

Similar question 3: Should we add branch protection to master?

See also. I'm a bit confused why this last one doesn't already happen, VSCode is supposed to detect when a branch is protected, is master not protected? nvm this is only for the web version.

[Joachim Breitner]

Maybe (additionally) the files themselves should be read-only in these directories?