5 commits

Author	SHA1	Message	Date
Johann150	a10b8875d9	run CI on pushes to main ... Since PRs seem to be much rarer than pushes to main, it makes more sense to do it this way. Perhaps in the future, it would make sense to run it on all pushes, but the question would be how PRs are handled.	2023-05-07 15:26:14 +02:00
Francis Dinh	bd11b9d818	Revert "ci: combine install and lint/build tasks" ... This reverts commit 759d031a5f. This was originally to solve some issues with builds during the workspace refactor in #86 but this didn't end up being the root cause, so it may actually be better to split these tasks again.	2022-09-07 14:02:45 -04:00
Francis Dinh	759d031a5f	ci: combine install and lint/build tasks	2022-08-26 15:50:20 -04:00
Chloe Kudryavtsev	20c0a7c6f4	chore: limit CI to PR only ... this is a temporary stopgap measure	2022-08-25 12:29:34 -04:00
Chloe Kudryavtsev	1506df3b94	chore(ci): add a dedicated build pipeline	2022-07-18 06:45:03 -04:00