test/include.mk: true is not '/bin/true` (#1813)

runtimeverification · May 13, 2020 · ce69262 · ce69262
1 parent a045a32
commit ce69262
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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