This repository was archived by the owner on Jan 24, 2022. It is now read-only.
Slightly improve the bash scripts#204
Merged
bors[bot] merged 2 commits intorust-embedded:masterfrom Sep 10, 2019
jonas-schievink:shell
Merged
Slightly improve the bash scripts#204bors[bot] merged 2 commits intorust-embedded:masterfrom jonas-schievink:shell
bors[bot] merged 2 commits intorust-embedded:masterfrom
jonas-schievink:shell
