contrib/configure-in-place

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