Commits on Oct 17, 2023

1. ci/contrib: do not fail on missing gh-pages …

   The current contrib deploy-hook fails if there is no `gh-pages` branch.
   Change the CI order to disregard the old `gh-pages` branch first.
   
   The `contrib` deploy-hook always creates a fresh `gh-pages` commit and
   pushes it out. However, currently it relies on the old `gh-pages` branch
   to exist, since it does not ignore errors when pruning it. Fortunately,
   the code always creates a new orphan branch, since it does not want to
   keep history for deployments. Therefore, we can simply use:
   
       `git worktree --orphan -B <branch> <path>`
   
   This will ensure to always create an orphan branch named `<branch>`, and
   override an existing branch if it exists (see `-b` vs `-B`). Hence,
   there is no need for us to prune the old branch, anymore.
   
   Since we will recreate the branch on every push, we have to explicitly
   specify the remote to push to. We no longer set up branch tracking.

   

   dvdhrm committed Oct 17, 2023
   Configuration menu

   • View commit details
   • Copy full SHA for 1d26183
   • Browse repository at this point

   Copy the full SHA

   1d26183 View commit details

   Browse the repository at this point in the history