Addressing #26#27
Conversation
There was a problem hiding this comment.
Pull request overview
Updates the Jupyter Book configuration to adjust how repository metadata and GitHub UI buttons (issues/repo/edit) are configured, likely to fix incorrect repository link behavior referenced by #26.
Changes:
- Changes
repository.path_to_bookfromdocsto.. - Moves GitHub button configuration into
sphinx.config.html_theme_optionsand enables the edit-page button. - Adds explicit
repository_url,repository_branch, andpath_to_docstheme options.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| search_bar_text: "Search..." | ||
| repository_url: https://github.com/transparency-certified/trace-specification | ||
| repository_branch: main | ||
| path_to_docs: docs |
There was a problem hiding this comment.
path_to_docs: docs is likely incorrect given this book is built from the repository root (jupyter-book build --all .) and the TOC references files as docs/.... With Sphinx docnames already including the docs/ prefix, setting path_to_docs to docs typically produces edit links like docs/docs/<page>.md. Consider setting path_to_docs to . (or removing it and relying on the repository.path_to_book/Jupyter Book defaults) so edit/repo links resolve correctly.
| path_to_docs: docs | |
| path_to_docs: . |
There was a problem hiding this comment.
This builds correctly locally, but may fail given how it is implemented on Github Pages. Let's leave it for now, and possibly revert it if it fails.
Another AI was not sure where this might be used elsewhere. So it might need to be put back in. Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
|
Pull request obsoleted by #32, but functionality in #26 not addressed @Xarthisius |
No description provided.