From c372f83fcb4aefff786d49fd35d4d7ebc3043b3a Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
Date: Sat, 28 Mar 2020 22:38:13 +0100
Subject: [PATCH] fix(detail): Add a newline

---
 entrypoint.sh | 2 +-
 timegroup.sh  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/entrypoint.sh b/entrypoint.sh
index 0a64dbe..ee4f41d 100755
--- a/entrypoint.sh
+++ b/entrypoint.sh
@@ -146,7 +146,7 @@ echo PACKAGE="$PACKAGE"
 docker run -i --init --rm --name=COQ -e PACKAGE="$PACKAGE" \
        -v "$HOST_WORKSPACE_REPO:$PWD" -w "$PWD" \
        "$COQ_IMAGE" /bin/bash --login -c "
-endGroup () {  init_opts=\"\$-\"; set +x; if [ -n \"\$startTime\" ]; then endTime=\$(date -u +%s); echo \"::endgroup::\"; printf \"↳ \"; date -u -d \"@\$((endTime - startTime))\" '+%-Hh %-Mm %-Ss'; unset startTime; else echo 'Error: missing startGroup command.'; case \"\$init_opts\" in  *x*) set -x ;; esac; return 1; fi; case \"\$init_opts\" in  *x*) set -x ;; esac; } ; startGroup () {  init_opts=\"\$-\"; set +x; if [ -n \"\$startTime\" ]; then endGroup; fi; if [ \$# -ge 1 ]; then groupTitle=\"\$*\"; else groupTitle=\"Unnamed group\"; fi; echo; echo \"::group::\$groupTitle\"; startTime=\$(date -u +%s); case \"\$init_opts\" in  *x*) set -x ;; esac; } # generated from helper.sh
+endGroup () {  init_opts=\"\$-\"; set +x; if [ -n \"\$startTime\" ]; then endTime=\$(date -u +%s); echo \"::endgroup::\"; printf \"↳ \"; date -u -d \"@\$((endTime - startTime))\" '+%-Hh %-Mm %-Ss'; echo; unset startTime; else echo 'Error: missing startGroup command.'; case \"\$init_opts\" in  *x*) set -x ;; esac; return 1; fi; case \"\$init_opts\" in  *x*) set -x ;; esac; } ; startGroup () {  init_opts=\"\$-\"; set +x; if [ -n \"\$startTime\" ]; then endGroup; fi; if [ \$# -ge 1 ]; then groupTitle=\"\$*\"; else groupTitle=\"Unnamed group\"; fi; echo; echo \"::group::\$groupTitle\"; startTime=\$(date -u +%s); case \"\$init_opts\" in  *x*) set -x ;; esac; } # generated from helper.sh
 export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '; set -ex
 $_OCAML407_COMMAND
 $_SCRIPT" script
diff --git a/timegroup.sh b/timegroup.sh
index 7c5a794..4d8ffa0 100755
--- a/timegroup.sh
+++ b/timegroup.sh
@@ -10,7 +10,7 @@ endGroup() {
         endTime=$(date -u +%s)
         echo "::endgroup::"
         # TZ=UTC-0 printf '↳%(%-Hh %-Mm %-Ss)T\n' "$((endTime - startTime))"  # not POSIX
-        printf "↳ "; date -u -d "@$((endTime - startTime))" '+%-Hh %-Mm %-Ss'
+        printf "↳ "; date -u -d "@$((endTime - startTime))" '+%-Hh %-Mm %-Ss'; echo
         # Assume the time difference < 24h
         unset startTime
     else