Skip to content

publish documentation as a github pages website - #147

Open
kevinushey wants to merge 1 commit into
laurikari:masterfrom
kevinushey:feature/github-pages
Open

publish documentation as a github pages website#147
kevinushey wants to merge 1 commit into
laurikari:masterfrom
kevinushey:feature/github-pages

Conversation

@kevinushey

Copy link
Copy Markdown

Summary

This adds an opt-in GitHub Actions workflow that publishes the project documentation as a GitHub Pages website at https://laurikari.github.io/tre/.

  • doc/build-website.sh assembles a small static site: it converts README.md into an index page with pandoc, and wraps doc/tre-api.html and doc/tre-syntax.html (which are body-only HTML fragments, presumably from the old tre.laurikari.com site template) in a minimal page template with a navigation header. The pages are styled with the existing doc/default.css.
  • .github/workflows/pages.yml runs the script on every push to master and deploys the result to GitHub Pages.

No existing files are modified, and nothing is published unless GitHub Pages is enabled for the repository (see below).

Activating (requires repo admin)

  1. Go to Settings -> Pages.
  2. Under "Build and deployment", set Source to GitHub Actions.
  3. Merge this PR. If it was merged before Pages was enabled, run the "Publish documentation" workflow manually from the Actions tab (or push any commit to master).

The site will then be live at https://laurikari.github.io/tre/ and will update automatically on every push to master.

Note: if this is merged while Pages is still disabled, the deploy job will fail on each push to master (harmless, but noisy). Either enable Pages, or disable the "Publish documentation" workflow from the Actions tab.

Testing

Built locally with pandoc 3.10 and verified that all three pages (index, API reference, regexp syntax) render as complete, styled HTML documents.

Possible follow-up, if there is interest: render the agrep man page (doc/agrep.1.in) to HTML as part of the site.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant