Skip to content

Conversation

avekens
Copy link
Contributor

@avekens avekens commented Dec 16, 2023

alignment with https://github.com/metamath/metamath-book (version from 15-Dez-2023).

alignment with https://github.com/metamath/metamath-book (version from 15-Dez-2023).
@digama0
Copy link
Member

digama0 commented Dec 16, 2023

I specifically spent time on the website build script to avoid this kind of duplication. We should decide where the pdf should live and not commit it in two places. The build script is capable of checking out multiple repositories and agglomerating the results.

@avekens
Copy link
Contributor Author

avekens commented Dec 16, 2023

I specifically spent time on the website build script to avoid this kind of duplication. We should decide where the pdf should live and not commit it in two places. The build script is capable of checking out multiple repositories and agglomerating the results.

Then I would propose to maintain the PDFs in https://github.com/metamath/metamath-book only.

@avekens
Copy link
Contributor Author

avekens commented Dec 22, 2023

Is there ary reason not to merge this PR now? I would like to have the versions in synch as soon as possible, and there is no plan to update the document in the near time. After it is decided where the PDF is finally located, it would be removed here or there anyway.

@digama0
Copy link
Member

digama0 commented Dec 22, 2023

Oops, sorry for the unclarity. I have a PR at metamath/metamath-book#248 doing the first part of the process to make metamath-book produce PDFs automatically and get them out of the repos entirely. Once that is merged we can remove metamath-german.pdf from this repo and download it directly from the release in the site build.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants