1. 05 Oct, 2020 2 commits
  2. 04 Oct, 2020 9 commits
  3. 18 Sep, 2020 6 commits
  4. 17 Sep, 2020 1 commit
  5. 16 Sep, 2020 1 commit
  6. 15 Sep, 2020 2 commits
  7. 14 Sep, 2020 2 commits
  8. 10 Sep, 2020 2 commits
  9. 09 Sep, 2020 5 commits
  10. 08 Sep, 2020 2 commits
  11. 01 Sep, 2020 1 commit
  12. 31 Aug, 2020 3 commits
  13. 29 Aug, 2020 1 commit
  14. 28 Aug, 2020 1 commit
  15. 27 Aug, 2020 1 commit
  16. 24 Aug, 2020 1 commit
    • azure: Remove job generating documentation · 7851a165
      With the recent addition of GitHub Actions to our CI infrastructure, we
      now have two jobs which generate documentation: once in GHA, once in
      Azure. Naturally, as they both want to update the same branch, they race
      against each other and one of both jobs will fail.
      
      Fix this by removing the documentation job from Azure.
      Patrick Steinhardt committed