diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/addsourcedir | 1 | ||||
| -rwxr-xr-x | contrib/configure-in-place | 26 | ||||
| -rwxr-xr-x | contrib/dimacs_to_smt.pl | 3 | ||||
| -rwxr-xr-x | contrib/get-authors | 1 | ||||
| -rwxr-xr-x | contrib/update-copyright.pl | 1 |
5 files changed, 31 insertions, 1 deletions
diff --git a/contrib/addsourcedir b/contrib/addsourcedir index ee507f0c6..8c7d74d90 100644 --- a/contrib/addsourcedir +++ b/contrib/addsourcedir @@ -2,6 +2,7 @@ # # addsourcedir # Morgan Deters <mdeters@cs.nyu.edu> for the CVC4 project +# Copyright (c) 2010 The CVC4 Project # # usage: addsourcedir paths... # diff --git a/contrib/configure-in-place b/contrib/configure-in-place new file mode 100755 index 000000000..09771676e --- /dev/null +++ b/contrib/configure-in-place @@ -0,0 +1,26 @@ +#!/bin/sh +# +# configure-in-place +# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2010 The CVC4 Project +# +# usage: configure-in-place [ arguments... ] +# +# This script configures CVC4 in the source directory (from where it +# should be invoked). +# + +if [ -e .svn ]; then + echo + echo "DO NOT USE THIS IN SUBVERSION 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 + +./configure "$@" +. builds/current +builds/$(CURRENT_BUILD)/config.status diff --git a/contrib/dimacs_to_smt.pl b/contrib/dimacs_to_smt.pl index 305db1d8e..6c1e0eeea 100755 --- a/contrib/dimacs_to_smt.pl +++ b/contrib/dimacs_to_smt.pl @@ -1,6 +1,7 @@ #!/usr/bin/perl -w # DIMACS to SMT -# Morgan Deters 2009 +# Morgan Deters +# Copyright (c) 2009, 2010 The CVC4 Project use strict; diff --git a/contrib/get-authors b/contrib/get-authors index 40aaf6a6d..dbe878d6b 100755 --- a/contrib/get-authors +++ b/contrib/get-authors @@ -2,6 +2,7 @@ # # get-authors # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2009, 2010 The CVC4 Project # # usage: get-authors [ files... ] # diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 22128ea6d..79e5986de 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -2,6 +2,7 @@ # # update-copyright.pl # Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2009, 2010 The CVC4 Project # # usage: update-copyright [ files/directories... ] # |