Tom Parker-Shemilt 0513259ff9 Realised that the Github actions default to the default branch for a repo ... (unlike Travis) and so the branch error isn't needed any more		2021-07-30 18:37:30 +01:00
..
bin	Update cleanup instructions	2020-02-24 22:38:19 +00:00
main.rs	Realised that the Github actions default to the default branch for a repo	2021-07-30 18:37:30 +01:00