diff options
Diffstat (limited to 'config')
| -rwxr-xr-x | config/mkbuilddir | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/config/mkbuilddir b/config/mkbuilddir index 1bc895548..252f17ea5 100755 --- a/config/mkbuilddir +++ b/config/mkbuilddir @@ -21,19 +21,19 @@ fi target=$1 build_type=$2 -echo Setting up "builds/$target/$build_type"... -rm -fv config.log config.status confdefs.h -mkdir -pv "builds/$target/$build_type" -ln -sfv "$target/$build_type/Makefile.builds" builds/Makefile +$as_echo "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 -echo Creating builds/current... +$as_echo "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 - echo Linking builds/$dir... - rm -f "builds/$dir" - ln -sfv "$target/$build_type/$dir" "builds/$dir" + $as_echo "Linking builds/$dir..." + $RM "builds/$dir" + $LN_S "$target/$build_type/$dir" "builds/$dir" done |