diff options
author | Karel Kočí <cynerd@email.cz> | 2015-05-05 11:58:26 +0200 |
---|---|---|
committer | Karel Kočí <cynerd@email.cz> | 2015-05-05 11:58:26 +0200 |
commit | dfe47d067a70f9781e3b431f6a685090bf87ff40 (patch) | |
tree | 5151ba40cdd422e9f9bbbba0398b2a569ba88311 /scripts/picosat-959/mkconfig | |
parent | 289b0ce128cdca79676307646eef3d56c25c6dd2 (diff) | |
download | linux-conf-perf-dfe47d067a70f9781e3b431f6a685090bf87ff40.tar.gz linux-conf-perf-dfe47d067a70f9781e3b431f6a685090bf87ff40.tar.bz2 linux-conf-perf-dfe47d067a70f9781e3b431f6a685090bf87ff40.zip |
Add picosat version 959
Diffstat (limited to 'scripts/picosat-959/mkconfig')
-rwxr-xr-x | scripts/picosat-959/mkconfig | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/scripts/picosat-959/mkconfig b/scripts/picosat-959/mkconfig new file mode 100755 index 0000000..d0c8fa8 --- /dev/null +++ b/scripts/picosat-959/mkconfig @@ -0,0 +1,35 @@ +#!/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 |