Stream: Coq devs & plugin devs

Topic: Permission denied during test-suite

view this post on Zulip Pierre Rousselin (Dec 29 2022 at 17:43):

Sorry, it's probably a noob question, but I have a problem when I try to run the test-suite on my machine (Fedora Linux):

Done: 99% (16507/16508, 1 left) (jobs: 1)File "ide/", line 1:
Error: I/O error: ide/fake_ide.cmx: Permission denied
make[1]: *** [Makefile:690 : ide/fake_ide.exe] Erreur 2
make[1]: *** Attente des tâches non terminées....

The files seem to have enough permissions though:

$ pwd
$ ls -ld ide ide/
drwxr-xr-x. 1 pierre pierre  1044 28 déc.  18:38 ide
-rw-rw-rw-. 1 pierre pierre 12347 16 déc.  08:47 ide/

Has anyone encountered the same problem?

Edit: Hmm... It seems the problem was coqide running during the tests... sorry.

Last updated: Jun 08 2023 at 04:01 UTC