Pierre Rousselin (Dec 29 2022 at 17:43): 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/fake_ide.ml", 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
/home/pierre/depots/coq/test-suite
$ ls -ld ide ide/fake_ide.ml
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/fake_ide.ml
Has anyone encountered the same problem?
Edit: Hmm... It seems the problem was coqide running during the tests... sorry.
Last updated: Sep 15 2024 at 13:02 UTC