Commits on Apr 5, 2023

1. CI: Fix configuration …

   1. Fix indentation (according to yamllint)
   2. Don't run CI on all push & pull request events. Pushing a commit to an open
      pull request would run each job twice.
   
      With the new configuration, we run CI once when opening a PR, and once when
      pushing a commit that belongs to a pull request. And once when merging to
      master (the `push` event). Importantly, this configuration still works for
      contributions from forked repositories, since the `pull_request` events are
      triggered on _our_ fork.

   

   bquorning committed Apr 5, 2023
   Configuration menu

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

   Copy the full SHA

   f7a194d View commit details

   Browse the repository at this point in the history