diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2019-02-28 11:56:19 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-03-10 20:10:32 +0000 |
commit | cf930214e12b49e89be4674043d9f461d667baae (patch) | |
tree | 90de5ea1c643d0d7ad2c5cf55e862d309e605d48 /scripts/build/install-local.sh | |
parent | b4d8fe0301b82e8abff0336bf6d1347dff11a853 (diff) | |
download | klee-cf930214e12b49e89be4674043d9f461d667baae.tar.gz |
Updated dependency build system for KLEE
Provide a single `scripts/build/build.sh` file to build KLEE and its dependencies.
Diffstat (limited to 'scripts/build/install-local.sh')
-rwxr-xr-x | scripts/build/install-local.sh | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/scripts/build/install-local.sh b/scripts/build/install-local.sh deleted file mode 100755 index 50dfb612..00000000 --- a/scripts/build/install-local.sh +++ /dev/null @@ -1,17 +0,0 @@ -#!/bin/bash -# Install all dependencies to build KLEE in a directory ${BASE} -set -e -if [[ "${BASE}x" == "x" ]]; then - echo "\${BASE} not set" - exit 1 -fi - -# Create base directory if not exists -mkdir -p "${BASE}" -DIR=$(dirname "$(readlink -f "$0" || stat -f "$0")") - -# Install dependencies -"${DIR}/install-klee-deps.sh" - -# Build KLEE -"${DIR}/klee.sh" |