From 429a2a8724f79f91814ecf9ec99daafd92df2c9d Mon Sep 17 00:00:00 2001
From: Martine Lenders <m.lenders@fu-berlin.de>
Date: Mon, 11 Jan 2021 14:13:16 +0100
Subject: [PATCH] github_annotate.sh: fix escaped echo for bash scripts

---
 dist/tools/ci/github_annotate.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dist/tools/ci/github_annotate.sh b/dist/tools/ci/github_annotate.sh
index 41acd65461..1e21802119 100644
--- a/dist/tools/ci/github_annotate.sh
+++ b/dist/tools/ci/github_annotate.sh
@@ -9,7 +9,7 @@ LOGFILE=
 OUTFILE=github_annotate_outfile.log
 ECHO_ESC=echo
 
-if ps -p $$ | grep -q '\<bash\>'; then
+if [ -n "${BASH_VERSION}" ]; then
     # workaround when included in bash to escape newlines and carriage returns
     # properly in _escape
     ECHO_ESC='echo -e'