diff options
Diffstat (limited to 'config/mkbuilddir')
-rwxr-xr-x | config/mkbuilddir | 45 |
1 files changed, 0 insertions, 45 deletions
diff --git a/config/mkbuilddir b/config/mkbuilddir deleted file mode 100755 index 87cd3460e..000000000 --- a/config/mkbuilddir +++ /dev/null @@ -1,45 +0,0 @@ -#!/bin/sh -# -# mkbuilddir -# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 -# -# usage: mkbuilddir target build-type -# -# Sets up the builds/ directory for building build-type for target: -# - removes configure detritus from top-level source directory -# - makes builds/$target/$build_type directory if it's not already there -# - links builds/Makefile to (possibly nonexistent) build Makefile -# - creates the builds/current Makefile include snippet -# - links builds/src and builds/test into build directory -# - -if [ $# -ne 2 ]; then - echo 'usage: mkbuilddir target build_type' >&2 - exit 1 -fi - -target=$1 -build_type=$2 - -: ${as_me:=mkbuilddir} -: ${as_echo:=echo} -: ${RM:=rm -f} -: ${MKDIR_P:=mkdir -p} -: ${LN_S:=ln -s} - -$as_echo "$as_me: Setting up builds/$target/$build_type..." -$RM config.log config.status confdefs.h builds/Makefile -$MKDIR_P "builds/$target/$build_type" -$LN_S "$target/$build_type/Makefile.builds" builds/Makefile - -$as_echo "$as_me: Creating builds/current..." -(echo "# This is the most-recently-configured CVC4 build"; \ - echo "# 'make' in the top-level source directory applies to this build"; \ - echo "CURRENT_BUILD = $target/$build_type") > builds/current - -for dir in src test; do - $as_echo "$as_me: Linking builds/$dir..." - $RM "builds/$dir" - $LN_S "$target/$build_type/$dir" "builds/$dir" -done - |