fix(detail): Add a newline

coq-community · Mar 28, 2020 · c372f83 · c372f83
1 parent 0ca1cfc
commit c372f83
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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