From cc4d2e41f5d72be55e2b506f45fa052e1b3d410b Mon Sep 17 00:00:00 2001
From: Jacob Bachmeyer <jcb@gnu.org>
Date: Fri, 16 Apr 2021 16:27:16 -0500
Subject: [PATCH] Replace non-portable `basename | sed` with Awk in dejagnu
 launcher

---
 ChangeLog |  7 +++++++
 dejagnu   | 15 ++++++++++++++-
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/ChangeLog b/ChangeLog
index cb7d0ef..77f89ab 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -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
diff --git a/dejagnu b/dejagnu
index ece4e09..c38dd4d 100755
--- a/dejagnu
+++ b/dejagnu
@@ -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