Files
Evan Martin 14cb84142d deploy doc
2024-06-25 11:45:48 -07:00

13 lines
295 B
Bash
Executable File

#!/bin/sh
# This script is used to deploy the website.
# It expects the `pages` branch to be checked out in the `deploy` subdir;
# set that up with:
# git worktree add deploy pages
set -e
make -C web profile=lto
(cd web && npm run build)
cp web/*.css web/*.html web/*.wasm web/*.png deploy