Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

links to md files are broken #128

Closed
Seasawher opened this issue Jan 14, 2024 · 5 comments · Fixed by #129 or #130
Closed

links to md files are broken #128

Seasawher opened this issue Jan 14, 2024 · 5 comments · Fixed by #129 or #130

Comments

@Seasawher
Copy link
Contributor

link to md file is now broken!

@Seasawher
Copy link
Contributor Author

Does the file used by pandoc have to be the README?
I think that creating a separate file that acts as a table of contents for pandoc would solve the problem of the broken link being placed in a visible place.

@Julian
Copy link
Collaborator

Julian commented Jan 14, 2024

https://github.com/leanprover-community/lean4-metaprogramming-book/blob/master/.github/workflows/book.yml#L29C1-L29C74 is the relevant line -- pandoc just wants the files in the order you want the output, and that line just uses the README to get that order, it doesn't care where the link goes, but it does need the filenames.

Any solution that gets the same list seems fine to me.

@Julian
Copy link
Collaborator

Julian commented Jan 14, 2024

(Including yeah removing it all from the README and just linking to the site, and having some side file meant for pandoc)

@Seasawher
Copy link
Contributor Author

By the way, solutions are missing in mdbook now. Should they be there?

@Julian
Copy link
Collaborator

Julian commented Jan 14, 2024

Yeah I guess it'd be nice if they show up at the end of the HTML book too.

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