Use gawk's gettimeofday if available #57 : fix for mawk

xonixx · Sep 27, 2021 · f884d69 · f884d69
1 parent 5fe2df1
commit f884d69
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Makesurefile b/Makesurefile
@@ -127,7 +127,7 @@
 @goal stable_version_prepared @private
   {
     echo '#!/bin/sh'
-    echo "if command -v gawk >/dev/null;then AWK='gawk -ltime -v Gawk=1'; X='';else AWK=awk; X=';function gettimeofday(){}';fi"
+    echo "if command -v gawk >/dev/null;then AWK='gawk -ltime -v Gawk=1'; X='';else AWK=awk; X='function gettimeofday(){}';fi"
     echo "exec \$AWK -v \"Version=$NEXT_VERSION\" -v \"Prog=\$0\" '"
     awk -v Q=\' '
 function trim(s) { sub(/^[ \t\r\n]+/, "", s); sub(/[ \t\r\n]+$/, "", s); return s }

diff --git a/makesure_stable b/makesure_stable
@@ -1,5 +1,5 @@
 #!/bin/sh
-if command -v gawk >/dev/null;then AWK='gawk -ltime -v Gawk=1'; X='';else AWK=awk; X=';function gettimeofday(){}';fi
+if command -v gawk >/dev/null;then AWK='gawk -ltime -v Gawk=1'; X='';else AWK=awk; X='function gettimeofday(){}';fi
 exec $AWK -v "Version=0.9.10" -v "Prog=$0" '
 BEGIN {
   Shell = "bash"