Skip to content

docs

docs #393

Workflow file for this run

# This is a basic workflow to help you get started with Actions
name: docs
# Controls when the workflow will run
on:
# Triggers the workflow on push or pull request events but only for the "master" branch
#push:
# branches: [ "master" ]
# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:
# run once a day
schedule:
- cron: '51 20 * * *'
concurrency:
group: docs
cancel-in-progress: false
# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
check-if-there-are-commits:
runs-on: ubuntu-latest
outputs:
commit_hash: ${{ steps.last-successful-commit.outputs.commit_hash }}
steps:
- uses: rhaas80/last-successful-commit-action@f23bb68905cacbe73dd5c91ee6c63dbb2a9bc265
id: last-successful-commit
with:
branch: 'master'
workflow_id: 'docs.yml'
github_token: ${{ secrets.GITHUB_TOKEN }}
build:
# don't run if nothing changed
needs: check-if-there-are-commits
if: ${{ github.event_name == 'workflow_dispatch' || needs.check-if-there-are-commits.outputs.commit_hash != github.sha }}
# The type of runner that the job will run on
# TODO: create custom docker image for this
runs-on: ubuntu-latest
# Steps represent a sequence of tasks that will be executed as part of the job
steps:
# Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
- uses: actions/checkout@v3
with:
fetch-depth: 1
submodules: recursive
# Runs a single command using the runners shell
- name: build documentation
run: |
set -e -x
echo "last successful build: " ${{ needs.check-if-there-are-commits.outputs.commit_hash }}
echo "sha: " ${{ github.sha }}
sudo apt-get update
sudo apt-get install make ghostscript texlive-plain-generic texlive-latex-recommended texlive-latex-extra curl
sudo apt-get clean
make AllDocHTML
make AllDocHTML # twice to get all references in LaTeX
# DEBUG code
# sudo apt-get install curl
# git submodule update --init flesh
# mkdir -p doc/HTML
# echo "Dummy" >doc/HTML/dummy.txt
# abuse a git tag to push out the HTML repo
cd doc/HTML
git init
git config user.email '[email protected]'
git config user.name 'GitHub runner'
git add --all
git commit -m 'nightly HTML docs'
git tag HTML
git remote add github https://x-access-token:${{ secrets.GITHUB_TOKEN }}@github.com/$GITHUB_REPOSITORY
git push -f github HTML
- name: Trigger update of HTML docs
run: curl -skL https://www.einsteintoolkit.org/update.php/?update