Clicking on the language manual, the pdf is linked to the master branch of the documentation. Documentation editing is what actually is maintained. To solve it: Change all the links to documentation that mention master. Delete the master documentation branch (minimize possibility of error). Check if pdf can be generated and checked for missing refs in a github action.
Clicking on the language manual, the pdf is linked to the master branch of the documentation. Documentation editing is what actually is maintained. To solve it: Change all the links to documentation that mention master. Delete the master documentation branch (minimize possibility of error). Check if pdf can be generated and checked for missing refs in a github action.