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

docs/dev: add page table-of-contents plugin #1275

Merged
merged 3 commits into from
May 15, 2023
Merged

Conversation

tzemanovic
Copy link
Member

@tzemanovic tzemanovic added documentation Improvements or additions to documentation CI skip-devnet-tests labels Apr 4, 2023
tzemanovic added a commit that referenced this pull request Apr 4, 2023
Fraccaman
Fraccaman previously approved these changes May 8, 2023
@adrianbrink
Copy link
Member

@tzemanovic Any idea why we one build failure?

@tzemanovic
Copy link
Member Author

@tzemanovic Any idea why we one build failure?

I think it will most likely pass after merge. It’s because the addition in the CI is not being used for the current CI run

@juped juped merged commit 6445f48 into main May 15, 2023
@juped juped deleted the tomas/docs/dev/pagetoc branch May 15, 2023 20:47
juped added a commit that referenced this pull request May 17, 2023
* main:
  changelog: add #1275
  CI/docs: add mdbook-pagetoc
  docs/dev: add mdbook-pagetoc plugin
  new chain id added
  Update documentation/docs/src/user-guide/ledger.md
  Update documentation/docs/src/user-guide/ledger.md
  docs are now up to date
  fixing docs
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CI documentation Improvements or additions to documentation
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants