Skip to content

Commit

Permalink
ci: Update GH pages manually
Browse files Browse the repository at this point in the history
I can't figure out why Travis stopped working, and I feel bad
freeloading off their compile time anyway, so here's a script to update
the GitHub pages by hand
  • Loading branch information
vEnhance committed Apr 24, 2024
1 parent 2c0e01f commit fd0907c
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 56 deletions.
56 changes: 0 additions & 56 deletions .travis.yml

This file was deleted.

31 changes: 31 additions & 0 deletions update-gh-pages.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
#!/bin/bash

set -euxo pipefail

SRCDIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" >/dev/null 2>&1 && pwd)"
TEMPDIR=/tmp/napkin-dist

cd "$SRCDIR"
latexmk

if [ ! -d "$TEMPDIR" ]; then
mkdir -p "$TEMPDIR"
fi
if [ ! -d "$TEMPDIR"/.git ]; then
cp -r .git/ "$TEMPDIR"
fi

cd $TEMPDIR
git checkout gh-pages

mkdir -p "$TEMPDIR"/asy

cd "$SRCDIR"
cp Napkin.log "$TEMPDIR"
cp Napkin.pdf "$TEMPDIR"
cp asy/*.asy "$TEMPDIR"/asy

cd "$TEMPDIR"
tree -H '.' -I "index.html" -D --charset utf-8 -T "An Infinitely Large Napkin" >index.html
git commit -a --amend -m "GitHub pages deploy from $(hostname) at $(date --utc)"
git diff --stat HEAD origin/gh-pages

0 comments on commit fd0907c

Please sign in to comment.