From 74ffa4eb40b5a924bebb342c368aebe722bf1277 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Wed, 13 May 2020 06:15:45 -0500 Subject: [PATCH] test/include.mk: `true` is not '/bin/true` --- test/include.mk | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/include.mk b/test/include.mk index 88bccdba17..a50827ef8a 100644 --- a/test/include.mk +++ b/test/include.mk @@ -71,7 +71,7 @@ $(DEF_KORE_DEFAULT): $(DEF_DIR)/$(DEF).k $(K) $(DIFF) $@.golden $@ || $(FAILED) %.verify.out: $(DEF_KORE_DEFAULT) - $(KORE_PARSER) $(DEF_KORE_DEFAULT) --verify >/dev/null 2>$@ || /bin/true + $(KORE_PARSER) $(DEF_KORE_DEFAULT) --verify >/dev/null 2>$@ || true $(DIFF) $@.golden $@ || $(FAILED) ### SEARCH