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: Nov 29 2023 at 21:01 UTC