diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-02-29 20:33:43 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-02-29 20:33:43 +0000 |
| commit | 2821b7a47e779c7d4f189ffdffaebe4bdb5b9036 (patch) | |
| tree | 16101f79b9c8927645fa896306c1e5cb83721332 /src/prop/bvpicosat/mkconfig | |
| parent | 9062483193f4ec9b38aaa57b228cae1fb551566a (diff) | |
This should fix the debian build fails:
* removed bvpicosat directory as it is currently not used
Cleared some of the flurry of warnings my previous merge caused in src/prop/
Diffstat (limited to 'src/prop/bvpicosat/mkconfig')
| -rwxr-xr-x | src/prop/bvpicosat/mkconfig | 35 |
1 files changed, 0 insertions, 35 deletions
diff --git a/src/prop/bvpicosat/mkconfig b/src/prop/bvpicosat/mkconfig deleted file mode 100755 index d0c8fa835..000000000 --- a/src/prop/bvpicosat/mkconfig +++ /dev/null @@ -1,35 +0,0 @@ -#!/bin/sh - -die () { - echo "*** mkconfig: $*" 1>&2 - exit 1 -} - -[ -f makefile ] || die "can not find 'makefile'" - -sed \ - -e '/^C[A-Z]*=/!d' \ - -e 's,^,#define PICOSAT_,' \ - -e 's,= *, ",' \ - -e 's,$,",' \ - makefile - -id="" -if [ -d .git -a -f .git/HEAD ] -then - head="`awk 'NF == 1' .git/HEAD`" - if [ x"$head" = x ] - then - head="`awk '{print $2}' .git/HEAD`" - if [ ! x"$head" = x -a -f ".git/$head" ] - then - id=" `cat .git/$head`" - fi - else - id=" $head" - fi -fi - -echo "#define PICOSAT_VERSION \"`cat VERSION`$id\"" - -exit 0 |