Closed xStrom closed 1 year ago
Ubuntu 18.04 in GitHub Actions was apparently removed in April. That's why our GitHub Pages job has been failing.
This PR updates the Ubuntu version which should make things run again.
I also took the opportunity to do a minor mdBook upgrade. Hopefully it works, we'll see once the job runs.
Ubuntu 18.04 in GitHub Actions was apparently removed in April. That's why our GitHub Pages job has been failing.
This PR updates the Ubuntu version which should make things run again.
I also took the opportunity to do a minor mdBook upgrade. Hopefully it works, we'll see once the job runs.