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"