Make use of GitHub CI#107
Merged
rptb1 merged 39 commits intomaster from branch/2023-01-11/github-ciJan 16, 2023
+530-48
Commits
Commits on Jan 11, 2023
- committed
- committed
- committed
- committed
Merge branch branch/2023-01-06/gcc-11.3.0-warnings into branch/2023-01-11/github-ci because these warnings cause GitHub CI to fail <https://github.com/Ravenbrook/mps/actions/runs/3892932541/jobs/66…
committed- committed
- committed
- committed
Visual Studio tools aren't in CMD in GitHub CI by default. Try using the shim we made for Travis CI.
committedTrying a path to Visual Studio environment documented by GitHub <https://github.com/actions/runner-images/blob/e6fcf60b8e6c0f80a065327eaefe836881c28b68/images/win/Windows2022-Readme.md?plain=1#L215>.
committed- committed
- committed
- committed
- committed
Commits on Jan 13, 2023
- committed
Explicitly excluding macOS on amd64 after observing it was included in <https://app.travis-ci.com/github/Ravenbrook/mps/builds/259659638>.
committedAnother attempt to suppress macOS on amd64, after observing it was still attempted in <https://app.travis-ci.com/github/Ravenbrook/mps/builds/259659638>.
committed
Commits on Jan 14, 2023
Commits on Jan 15, 2023
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed