Unnamed repository; edit this file 'description' to name the repository.
Auto merge of #3514 - RalfJung:hyperfine, r=RalfJung
CI: run benches with hyperfine rather than bash
The hyperfine installation is cached so this should not cost a lot of CI time.
This is step 1/2 to getting rid of the BASH variable hack.
