blob: 81517cfe43546f1d73a9eec6ec4efefb8ba8bcce (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
#!/bin/bash -ex
#
# configure-in-place
# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
# Copyright (c) 2010-2013 The CVC4 Project
#
# usage: configure-in-place [ arguments... ]
#
# This script configures CVC4 in the source directory (from where it
# should be invoked).
#
if [ -e .git ] && ! [ x"$1" = x-f ]; then
echo
echo "DO NOT USE THIS IN GIT WORKING DIRECTORIES!"
echo
echo "You might accidentally commit Makefiles in the source directories"
echo "improperly, since they exist in the source directory for"
echo "another purpose."
echo
exit 1
fi
if [ x"$1" = x-f ]; then
shift
fi
./configure "$@"
CURRENT_BUILD="$(grep '^CURRENT_BUILD *= *' builds/current | awk 'BEGIN {FS=" *= *"} {print$2}')"
builds/$CURRENT_BUILD/config.status
|