diff options
Diffstat (limited to 'dejagnu')
-rwxr-xr-x | dejagnu | 15 |
1 files changed, 14 insertions, 1 deletions
@@ -147,7 +147,20 @@ if $want_version ; then fi # Remove any leading autoconf platform prefix and the "dejagnu" prefix. -command=`basename "$0" | sed -e 's/^.*-\?dejagnu-\?//'` +# command=`basename "$0" | sed -e 's/^.*-\?dejagnu-\?//'` +# The above simple solution is not portable, so we use Awk: +command=`echo "$0" | awk 'BEGIN { FS = "/" } +{ OFS = FS = "-" + $0 = $NF + for (i = 1; i <= NF; i++) if ($i ~ /dejagnu/) break; + for (j = 1; j <= (NF - i); j++) $j = $(j+i); + NF = j - 1 + print }'` +# Initially splitting on "/", then assigning the last field to the record +# performs the role of basename. Splitting on "-" and searching for a +# field matching /dejagnu/ identifies the other prefixes, and the second +# loop removes the "dejagnu" prefix and everything before it. The record +# is then truncated, printed, and thereby returned to the shell. while expr $# \> 0 > /dev/null do |