This PR adds a Github action workflow to deploy the book. This workflow is triggered when a commit is pushed to master. Then, the book is built on some Github server and the built content is pushed to the gh-pages branch.
The main advantage is that you no longer keep the book's built version on the main branches. This 1) makes the change history cleaner, since there are no duplicate changes (i.e., source file and book files) and 2) the book doesn't need to be built by someone whenever a change is merged, making e.g., typo fixes and other contributions much more convenient.
This PR adds a Github action workflow to deploy the book. This workflow is triggered when a commit is pushed to master. Then, the book is built on some Github server and the built content is pushed to the
gh-pagesbranch.The main advantage is that you no longer keep the book's built version on the main branches. This 1) makes the change history cleaner, since there are no duplicate changes (i.e., source file and book files) and 2) the book doesn't need to be built by someone whenever a change is merged, making e.g., typo fixes and other contributions much more convenient.
(To be discussed on Monday.)