Is that intended? The testsuite failed looking for a Python script under _install_ci
— and this seems to go away after dune install --prefix=$PWD/_install_ci coq-core coq-stdlib coqide-server coq coqide
Probably not. I'm not sure what would justify this path being hard-coded anywhere, but even if it were justified for CI for some reason, it should not create failures in the case of other setups.
Last updated: Dec 07 2023 at 14:02 UTC