From f85ad74a0516db1abb8839714cd2330d82eed9fa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C8=98tefan=20Talpalaru?= Date: Wed, 19 Jan 2022 21:44:33 +0100 Subject: [PATCH] /dev/tty exists but can't be used in GitHub Actions (#35) --- makefiles/targets.mk | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/makefiles/targets.mk b/makefiles/targets.mk index 2cc2d60..0d37685 100644 --- a/makefiles/targets.mk +++ b/makefiles/targets.mk @@ -85,7 +85,7 @@ build-nim: | sanity-checks # Check if the update might cause loss of work. Abort, if so, while allowing an override mechanism. update-test: - TEE_TO_TTY="cat"; if [[ -e /dev/tty ]]; then TEE_TO_TTY="tee /dev/tty"; fi; \ + TEE_TO_TTY="cat"; if bash -c ": >/dev/tty" &>/dev/null; then TEE_TO_TTY="tee /dev/tty"; fi; \ COMMAND="git status --short --untracked-files=no --ignore-submodules=untracked"; \ LINES=$$({ $${COMMAND} | grep 'vendor' && echo ^---top level || true; git submodule foreach --recursive --quiet "$${COMMAND} | grep . && echo ^---\$$name || true"; } | $${TEE_TO_TTY} | wc -l); \ if [[ "$${LINES}" -ne "0" && "$(OVERRIDE)" != "1" ]]; then echo -e "\nYou have uncommitted local changes which might be overwritten by the update. Aborting.\nIf you know better, you can re-run the command with OVERRIDE=1.\n"; exit 1; fi