diff --git a/build.sh b/build.sh index 80a6b610eff126619ec32f14b5ea6390b86d15ab..7f94a22d775d540cb2160b2fc23640f6276fa3a4 100755 --- a/build.sh +++ b/build.sh @@ -270,15 +270,7 @@ set_doc_headers cd $top if [ $sparse == 1 -o $smatch == 1 -o ! -d smatch ]; then - if [ ! -d smatch ]; then - echo 'Smatch missing, run prepare_build.sh first' - exit 1 - fi - cd smatch - git remote update - git reset --hard origin/master - make -j HAVE_LLVM=no - cd .. + build_smatch origin/master fi export CCACHE_MAXSIZE=512M diff --git a/funcs.sh b/funcs.sh index a0095a58983d932ff55d0d35f5b1136d0ca711a2..a71c9c026aec4dad2ed0ad2611cdfe9478f1005c 100755 --- a/funcs.sh +++ b/funcs.sh @@ -78,6 +78,19 @@ function strip_top() sed "s;$top/media-git/;;g" } +function build_smatch() +{ + if [ ! -d smatch ]; then + echo '`smatch` folder missing, run prepare_build.sh first' + exit 1 + fi + cd smatch + git remote update + git reset --hard $1 + make -j HAVE_LLVM=no + cd .. + return 0 +} function setup() { if [ ! -d media-git ]; then @@ -98,9 +111,7 @@ function setup() git remote update git checkout -b build-test media_stage/master cd .. - git clone $smatch_git - cd smatch - make -j HAVE_LLVM=no + build_smatch origin/master exit 0 }