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