Tests fail to pass because of strange redirection

Question

Tests fail to pass because of strange redirection

Closed this issue a year ago · 1 comments

Coq tests do not pass, because of a problem in tests/Makefile.shared l.112:

	@if ! $(COQC) $(COQ_PROOF_FILE) &> $(TMP_FILE); then

The & seems to be erroneous, did you meant > $(TMP_FILE) 2>&1 ?

Answer 1 · 2023-06-22T13:08:46.000Z

Ah, I think that the main problem is that &> is bash-specific (see e.g. this), and does not work for sh (I always get tricked because sh is aliased to bash on my distro). Using > ... 2>&1 instead would probably be the good solution to make it work for sh too, would you have the time to submit a PR for that ?