Replace old GitHub action with updated one.#247

Merged

timja merged 9 commits intomasterfrom github-ci

Mar 4, 2024

+85-87

Commits on Feb 27, 2024

Replace old GitHub action with updated one.
uhafner
committed

Commits on Feb 29, 2024

Always print the time, even if < 1ms.
uhafner
committed