Did lean file permissions change recently?

Stream: general

[Jason Rute]

Did the .lean file permissions change recently for the lean files in the core library? They used to be "-rw-r--r--", but I think they are now "-r--r--r--". (In other words, you can know longer modify the files.) I think this is good because I've accidentally modified such files in the past (and I think it would make sense to do the same for the mathlib .lean files in _target). However, it also breaks some hacky proof recording stuff I made for lean-gptf. That isn't a big deal. I'll fix it. I just want to understand what is going on here. :smile:.

[Gabriel Ebner]

Are you using elan? I believe this feature is thanks to the following PR: https://github.com/leanprover/elan/pull/27

[Jason Rute]

Yes elan. Thanks! This explains it. :smile: