Stream: Coq devs & plugin devs

Topic: Why are some `.v` files listed as executable in the stdlib?


view this post on Zulip Pierre Rousselin (Sep 11 2023 at 14:04):

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)?

view this post on Zulip Gaëtan Gilbert (Sep 11 2023 at 14:08):

probably no good reason
It's hard to see permissions in most commit / diff views AFAIK so easy to miss it

view this post on Zulip Emilio Jesús Gallego Arias (Sep 11 2023 at 20:10):

Yup, that was likely not intended, a PR to fix it should be pretty simple.


Last updated: Apr 14 2024 at 09:39 UTC