On my local repo, the following files have x
permission. This is bizarre.
$ find . -type f -perm /u+x
./Logic/Adjointification.v
./Reals/Rtrigo_facts.v
$ ls -l $(find . -type f -perm /u+x)
-rwxr-xr-x. 1 pierre pierre 4434 16 déc. 2022 ./Logic/Adjointification.v
-rwxr-xr-x. 1 pierre pierre 6753 4 févr. 2023 ./Reals/Rtrigo_facts.v
Is it only for me? Is there a good reason (though, I cannot imagine any)?
probably no good reason
It's hard to see permissions in most commit / diff views AFAIK so easy to miss it
Yup, that was likely not intended, a PR to fix it should be pretty simple.
Last updated: Oct 13 2024 at 01:02 UTC