Skip to content

publish documentation as a github pages website #147

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.

Sign up for GitHub

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

Open
kevinushey wants to merge 1 commit into
base: master
Choose a base branch
from
Open

publish documentation as a github pages website #147

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 44 additions & 0 deletions .github/workflows/pages.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
name: Publish documentation

on:
push:
branches: [ master ]
workflow_dispatch:

permissions:
contents: read
pages: write
id-token: write

concurrency:
group: pages
cancel-in-progress: true

jobs:
build:
name: Build website
runs-on: ubuntu-latest
steps:
- name: Prepare
run: |
sudo apt-get update
sudo apt-get install -y pandoc
- name: Check out
uses: actions/checkout@v4
- name: Build website
run: ./doc/build-website.sh _site
- name: Upload website
uses: actions/upload-pages-artifact@v3
with:
path: _site
deploy:
name: Deploy to GitHub Pages
needs: build
runs-on: ubuntu-latest
environment:
name: github-pages
url: ${{ steps.deployment.outputs.page_url }}
steps:
- name: Deploy
id: deployment
uses: actions/deploy-pages@v4
79 changes: 79 additions & 0 deletions doc/build-website.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
#! /bin/sh
#
# Assembles the documentation website published via GitHub Pages.
# Requires pandoc, which is used to convert README.md to HTML.
#
# Usage: doc/build-website.sh [output-directory]
#

set -e

srcdir=`dirname "$0"`
outdir=${1:-_site}

if ! command -v pandoc > /dev/null 2>&1; then
echo "error: pandoc is required to build the website" >&2
exit 1
fi

mkdir -p "$outdir"
cp "$srcdir/default.css" "$outdir"

# The HTML files in doc/ are body fragments with no <html> or <head>;
# they were originally embedded in a site template. This wraps a
# fragment (read from stdin) into a complete page.
emit_page() {
title=$1
out=$2

{
cat << EOF
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>$title</title>
<link rel="stylesheet" href="default.css">
<style>
body {
max-width: 50em;
margin: 0 auto;
padding: 0 1em 2em 1em;
font-family: sans-serif;
line-height: 1.5;
}
nav.site {
border-bottom: 1px solid #cbc5b8;
padding: 0.5em 0;
margin-bottom: 1.5em;
}
nav.site a {
margin-right: 1em;
}
</style>
</head>
<body>
<nav class="site">
<a href="index.html">TRE</a>
<a href="tre-api.html">API reference</a>
<a href="tre-syntax.html">Regexp syntax</a>
<a href="https://github.com/laurikari/tre">GitHub</a>
</nav>
EOF
cat
cat << EOF
</body>
</html>
EOF
} > "$out"
}

pandoc --from gfm --to html "$srcdir/../README.md" \
| emit_page "TRE" "$outdir/index.html"

emit_page "TRE API reference manual" "$outdir/tre-api.html" \
< "$srcdir/tre-api.html"

emit_page "TRE Regexp Syntax" "$outdir/tre-syntax.html" \
< "$srcdir/tre-syntax.html"