From 80603a256df7193f84706bc234ea738510bdbce7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 28 Feb 2020 09:28:41 +0100
Subject: [PATCH] chore: fix benchmark once more

Github Actions' `sh` doesn't seem to like `echo -e`
---
 tests/bench/speedcenter.exec.yaml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/bench/speedcenter.exec.yaml b/tests/bench/speedcenter.exec.yaml
index 71dc765146..55e94e6631 100644
--- a/tests/bench/speedcenter.exec.yaml
+++ b/tests/bench/speedcenter.exec.yaml
@@ -48,8 +48,8 @@
     cwd: ../compiler/
     cmd: |
       set -eu
-      echo -n 'sum binary sizes: '
-      for f in *.lean; do ../bench/compile.sh $f; echo -ne "$f.out\0"; done | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
+      printf 'sum binary sizes: '
+      for f in *.lean; do ../bench/compile.sh $f; printf '%s\0' "$f.out"; done | wc -c --files0-from=- | tail -1 | cut -d' ' -f 1
     max_runs: 1
     runner: output
 - attributes: