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: Jun 04 2023 at 19:30 UTC