merge from dev

This commit is contained in:
Daan Leijen 2022-12-19 17:08:45 -08:00
commit 92ffc25d79
65 changed files with 793 additions and 741 deletions

View file

@ -13,7 +13,7 @@ trigger:
include:
- v*
jobs:
jobs:
- job:
displayName: Windows
pool: