Eli Schwartz
2edcbb452e
CI: trigger website job when testing modifications to the website job
1 year ago
Eli Schwartz
9153b82cc2
CI: add pip caching to website job
...
On average, saves 20 seconds for a job that may take 1.5 or 2 minutes.
Mostly due to recompiling the same 3 wheels again and again, so that
avoids pointless CPU waste.
1 year ago
Eli Schwartz
f3635ff50d
avoid re-uploading the docs when a PR is based on the upstream repo
...
In this case, we have the secret available, and the workflow ran even
though it wasn't on branch "master" because of the pull request trigger.
Since the change hasn't landed on master, though, we do not want to
update the website. So check for pushes to master, specifically.
2 years ago
Alex
9074ad93c6
build: harden workflow permissions
...
Signed-off-by: Alex <aleksandrosansan@gmail.com>
2 years ago
Eli Schwartz
01c8205864
github workflows: upgrade actions/checkout to version 3
...
This is a no-op change, but github complains that nodejs is outdated if
you don't. It's not obvious why this required a major version bump...
2 years ago
Stone Tickle
71ea9e3d4c
add man page generation to build
3 years ago
Christian Clauss
a5020857f3
Fix typos discovered by codespell
3 years ago
Daniel Mensinger
0eec5480fb
docs: Also check on pull-requests
3 years ago
Daniel Mensinger
2ab5620769
docs: GitHub Action up the JSON docs
3 years ago
Xavier Claessens
9d3e9c43cc
ci: Add comment to not forget updating wrapdb rules
3 years ago
Daniel Mensinger
de32802ee4
docs: Fix the GitHub action
3 years ago
Daniel Mensinger
cab77b0e4c
ci: Use GitHub concurrency
3 years ago
Jon Turney
1ab0694556
CI: Don't try to update website in a forked repository
4 years ago
Xavier Claessens
4dec7dbb71
ci: Automatically update website when pushing to master
4 years ago