Rebuild documentation website

Rebuilding the documentation website is a manual action:

Instructions

  1. Visit the root documentation project repository on GitHub in your browser.

  2. Click Actions in the top toolbar.

  3. You should now be presented this screen:

    trigger git workflow publish gh pages

    1. Select the action Publish to GitHub Pages on the left sidebar.

    2. Click the Run workflow button, and then the green Run workflow button.

  4. This will create a new run. Its status is indicated by the icon prefixing the line. As soon as it turns green, the new site is built and deployed.

Sometimes when you refresh the documentation website in your browser, the new changes won’t show up. Oftentimes cache is the culprit here. Try hard reloading the page in your browser, for example pressing Ctrl+Shift+R in Google Chrome.