From 907d5301ee8200a79c39a3594521d1b81e046306 Mon Sep 17 00:00:00 2001 From: Steffen Jaeckel Date: Fri, 23 Jun 2017 16:46:31 +0200 Subject: [PATCH] update coverity build script to use makefile.unix it seems like the regular makefile is somehow broken... --- coverity.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coverity.sh b/coverity.sh index 0c919388b..8f3059628 100755 --- a/coverity.sh +++ b/coverity.sh @@ -16,7 +16,7 @@ myCflags="" myCflags="$myCflags -O2 ${2}" myCflags="$myCflags -pipe -Werror -Wpointer-arith -Winit-self -Wextra -Wall -Wformat -Wformat-security" -CFLAGS="$myCflags" cov-build --dir cov-int make -f makefile -j3 IGNORE_SPEED=1 1>gcc_1.txt +CFLAGS="$myCflags" cov-build --dir cov-int make -f makefile.unix $MAKE_OPTS IGNORE_SPEED=1 1>gcc_1.txt if [ $? -ne 0 ] then