diff options
-rw-r--r-- | ChangeLog | 7 | ||||
-rwxr-xr-x | dejagnu | 15 |
2 files changed, 21 insertions, 1 deletions
@@ -1,3 +1,10 @@ +2021-04-16 Jacob Bachmeyer <jcb@gnu.org> + + PR47382 + + * dejagnu (command): Use Awk instead of non-portable basename(1) + and a non-portable sed(1) pattern to initially set this variable. + 2021-04-15 Jacob Bachmeyer <jcb@gnu.org> PR47382 @@ -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 |