Fix #18836

[ana-borges]

Fix for #18836.

CoqIDE also seemed to be affected.

[ejgallego]

Thanks @ana-borges , the fix should only be needed for Coq 8.10-8.13 tho, let me actually check when this problem was introduced.

[ejgallego]

Thanks for the patch @ana-borges , however this fix is only needed for Coq 8.12.x and Coq 8.13.x ; I thus suggest you amend the PR.

[ejgallego]

Also, I'd suggest you update the PR / commit message to fixes #18836 , so Github will link this patch to the issue it is solving

[ana-borges]

this fix is only needed for Coq 8.12.x and Coq 8.13.x ; I thus suggest you amend the PR.

Thank you for checking @ejgallego.

Did you also check CoqIDE? I tried checking again and couldn't install it with or without COQ_USE_DUNE, probably for an unrelated reason (I remember not being able to install last year either). So I may easily have been wrong yesterday when I concluded this problem affected it as well.

[ejgallego]

Thanks @ana-borges , indeed coqide packages need the same fix; well-spotted.

[mseri]

@ejgallego is this ready to merge?

[ana-borges]

@mseri: There are a bunch of CI failures, which I guess should be fixed before merging, right?

I failed to reproduce the errors due to not being able to install all dependencies, and then I got busy with other stuff and couldn't pick this up again. Next week I will have more time. If you or anyone has some insight on the errors, I would appreciate it.

[mseri]

All the failures are related to missing or incorrect system packages, we cannot do anything to solve them. I'll postpone deciding the merge to next week after you had time to have a look. Thanks for the prompt response

[ejgallego]

Indeed, this looks good, thanks @ana-borges !

[ana-borges]

@mseri Ok, I see that these errors were already there. Thank you for pointing this out. Feel free to merge!

[mseri]

Thanks both for the help