michael@1: #! /bin/sh
michael@1: ##
michael@1: ##  devtool -- Development Tool
michael@1: ##  Copyright (c) 2001-2002 Ralf S. Engelschall <rse@engelschall.com>
michael@1: ##
michael@1: 
michael@1: if [ $# -eq 0 ]; then
michael@1:     echo "devtool:USAGE: devtool <command> [<arg> ...]" 1>&2
michael@1:     exit 1
michael@1: fi
michael@1: 
michael@1: cmd="$1"
michael@1: shift
michael@1: 
michael@1: devtoolfunc="./devtool.func"
michael@1: 
michael@1: if [ ! -f devtool.conf ]; then
michael@1:     echo "devtool:ERROR: no devtool.conf in current directory" 1>&2
michael@1:     exit 1
michael@1: fi
michael@1: 
michael@1: cmdline=`grep "^%$cmd" devtool.conf`
michael@1: if [ ".$cmdline" = . ]; then
michael@1:     echo "devtool:ERROR: command $cmd not found in devtool.conf" 1>&2
michael@1:     exit 1
michael@1: fi
michael@1: 
michael@1: if [ ".$TMPDIR" != . ]; then
michael@1:     tmpdir="$TMPDIR"
michael@1: elif [ ".$TEMPDIR" != . ]; then
michael@1:     tmpdir="$TEMPDIR"
michael@1: else
michael@1:     tmpdir="/tmp"
michael@1: fi
michael@1: tmpfile="$tmpdir/as-gui.$$.tmp"
michael@1: 
michael@1: rm -f $tmpfile
michael@1: touch $tmpfile
michael@1: echo ". $devtoolfunc" >>$tmpfile
michael@1: ( sed <devtool.conf -e "1,/^%common/d" -e '/^%.*/,$d'
michael@1:   sed <devtool.conf -e "1,/^%$cmd/d" -e '/^%.*/,$d' ) |\
michael@1: sed -e 's;\([ 	]\)@\([a-zA-Z_][a-zA-Z0-9_]*\);\1devtool_\2;' >>$tmpfile
michael@1: 
michael@1: sh $tmpfile "$@"
michael@1: 
michael@1: rm -f $tmpfile >/dev/null 2>&1 || true