Skip to content

How to Update Developer Documentation

All changes to the developer documentation are managed through the GitHub Wiki.
There are three common scenarios:

  • Editing an existing page

    1. Make your changes directly in the Wiki page.

    2. Updates will automatically appear in the GitHub Pages documentation.

    3. The documentation site is rebuilt every Saturday via a CI workflow.

  • Adding a new page

    1. Use the “New Page” option in the GitHub Wiki to create your page.
    2. Once that is done, add the page to the Wiki Sidebar by editing the Sidebar.md file.
    3. Ensure the sidebar entry correctly links to your new Wiki page.

  • Removing a page

    1. Delete the page from the Wiki.
    2. Remove any references to it in the Sidebar or elsewhere in the Wiki.

Important:
If a Wiki page is not linked in the Sidebar, it will not appear in the published documentation.

  • The documentation site updates automatically every Saturday.

  • During each update, the CI workflow checks for broken links.

  • If broken links are found, the workflow will fail (but the documentation will still be published).

Triggering Manual Updates

If you need the documentation updated immediately (instead of waiting until Saturday), you can manually trigger the CI workflow in GitHub Actions.