As-gui Sources: devtool@0e0eb7c91312

     1 #! /bin/sh

     2 ##

     3 ##  devtool -- Development Tool

     4 ##  Copyright (c) 2001-2002 Ralf S. Engelschall <rse@engelschall.com>

     5 ##

     7 if [ $# -eq 0 ]; then

     8     echo "devtool:USAGE: devtool <command> [<arg> ...]" 1>&2

     9     exit 1

    10 fi

    12 cmd="$1"

    13 shift

    15 devtoolfunc="./devtool.func"

    17 if [ ! -f devtool.conf ]; then

    18     echo "devtool:ERROR: no devtool.conf in current directory" 1>&2

    19     exit 1

    20 fi

    22 cmdline=`grep "^%$cmd" devtool.conf`

    23 if [ ".$cmdline" = . ]; then

    24     echo "devtool:ERROR: command $cmd not found in devtool.conf" 1>&2

    25     exit 1

    26 fi

    28 if [ ".$TMPDIR" != . ]; then

    29     tmpdir="$TMPDIR"

    30 elif [ ".$TEMPDIR" != . ]; then

    31     tmpdir="$TEMPDIR"

    32 else

    33     tmpdir="/tmp"

    34 fi

    35 tmpfile="$tmpdir/as-gui.$$.tmp"

    37 rm -f $tmpfile

    38 touch $tmpfile

    39 echo ". $devtoolfunc" >>$tmpfile

    40 ( sed <devtool.conf -e "1,/^%common/d" -e '/^%.*/,$d'

    41   sed <devtool.conf -e "1,/^%$cmd/d" -e '/^%.*/,$d' ) |\

    42 sed -e 's;\([ 	]\)@\([a-zA-Z_][a-zA-Z0-9_]*\);\1devtool_\2;' >>$tmpfile

    44 sh $tmpfile "$@"

    46 rm -f $tmpfile >/dev/null 2>&1 || true

As-gui Sources / file revision