1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/devtool Fri Nov 28 11:21:08 2008 +0100
1.3 @@ -0,0 +1,46 @@
1.4 +#! /bin/sh
1.5 +##
1.6 +## devtool -- Development Tool
1.7 +## Copyright (c) 2001-2002 Ralf S. Engelschall <rse@engelschall.com>
1.8 +##
1.9 +
1.10 +if [ $# -eq 0 ]; then
1.11 + echo "devtool:USAGE: devtool <command> [<arg> ...]" 1>&2
1.12 + exit 1
1.13 +fi
1.14 +
1.15 +cmd="$1"
1.16 +shift
1.17 +
1.18 +devtoolfunc="./devtool.func"
1.19 +
1.20 +if [ ! -f devtool.conf ]; then
1.21 + echo "devtool:ERROR: no devtool.conf in current directory" 1>&2
1.22 + exit 1
1.23 +fi
1.24 +
1.25 +cmdline=`grep "^%$cmd" devtool.conf`
1.26 +if [ ".$cmdline" = . ]; then
1.27 + echo "devtool:ERROR: command $cmd not found in devtool.conf" 1>&2
1.28 + exit 1
1.29 +fi
1.30 +
1.31 +if [ ".$TMPDIR" != . ]; then
1.32 + tmpdir="$TMPDIR"
1.33 +elif [ ".$TEMPDIR" != . ]; then
1.34 + tmpdir="$TEMPDIR"
1.35 +else
1.36 + tmpdir="/tmp"
1.37 +fi
1.38 +tmpfile="$tmpdir/as-gui.$$.tmp"
1.39 +
1.40 +rm -f $tmpfile
1.41 +touch $tmpfile
1.42 +echo ". $devtoolfunc" >>$tmpfile
1.43 +( sed <devtool.conf -e "1,/^%common/d" -e '/^%.*/,$d'
1.44 + sed <devtool.conf -e "1,/^%$cmd/d" -e '/^%.*/,$d' ) |\
1.45 +sed -e 's;\([ ]\)@\([a-zA-Z_][a-zA-Z0-9_]*\);\1devtool_\2;' >>$tmpfile
1.46 +
1.47 +sh $tmpfile "$@"
1.48 +
1.49 +rm -f $tmpfile >/dev/null 2>&1 || true
