Stream: Coq devs & plugin devs

Topic: Dune Test suite Failure


view this post on Zulip Janno (May 18 2020 at 13:35):

I am trying to run make -f Makefile.dune test-suite and it all seems to be going well until this here happens:

GEN output/MExtraction.out
/bin/sh: 1: cannot create output/MExtraction.out: Permission denied

Is this a known problem? I couldn't find anything on the bug tracker.

view this post on Zulip Théo Zimmermann (May 18 2020 at 13:36):

I don't know how widely known this is but FTR I get the same failure.

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 13:37):

Yes, there is a bug open for this; the fix is easy, actually let me submit it right now

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 13:37):

Sorry for the dealy

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2020 at 16:19):

@Janno should be better now, let us know if there are further problems


Last updated: Oct 16 2021 at 02:03 UTC