diff options
| author |  Alexey Yakovenko <wakeroid@gmail.com> | 2010-05-27 22:51:35 +0200 |
|---|---|---|
| committer | Alexey Yakovenko <wakeroid@gmail.com> | 2010-05-27 22:51:35 +0200 |
| commit | 4810f9a0af507bb405e6a3c58decfa9c9980b2ff (patch) | |
| tree | 75ac9c06345b23528e6771bb1bae697ff5c29c1c /plugins/dumb/dumb-kode54/make/config.sh | |
| parent | ad71971955594ada4a0b14d176a192d050c9ee36 (diff) | |
merged parts of DUMB-0.9.3
Diffstat (limited to 'plugins/dumb/dumb-kode54/make/config.sh')
| -rw-r--r-- | plugins/dumb/dumb-kode54/make/config.sh | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/plugins/dumb/dumb-kode54/make/config.sh b/plugins/dumb/dumb-kode54/make/config.sh index 923b3ccc..9be5e49c 100644 --- a/plugins/dumb/dumb-kode54/make/config.sh +++ b/plugins/dumb/dumb-kode54/make/config.sh @@ -5,7 +5,7 @@ # should be run indirectly through the 'make config' target (or the 'make'
# target the first time).
-if [ ! -e make/dumbask ]; then
+if [ ! -f make/dumbask ]; then
echo "You should not be running this directly! Use 'make' or 'make config'."
exit
fi
@@ -24,7 +24,9 @@ echo "Please specify an installation prefix (default $DEFAULT_PREFIX)." echo -n '> '
read PREFIX
if [ -z $PREFIX ]; then PREFIX=$DEFAULT_PREFIX; fi
-echo "PREFIX := $PREFIX" >> make/config.tmp
+echo "PREFIX := `echo "$PREFIX" | \
+ sed -e 's/\${\([A-Za-z_][A-Za-z0-9_]*\)}/$(\1)/g' \
+ -e 's/\$\([A-Za-z_][A-Za-z0-9_]*\)/$(\1)/g'`" >> make/config.tmp
fi
mv -f make/config.tmp make/config.txt
|