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

Makesurefile

@@ -127,15 +127,15 @@
 @goal stable_version_prepared @private
   {
     echo '#!/bin/sh'
-    echo "command -v gawk >/dev/null && AWK='gawk -ltime -v Gawk=1' || AWK=awk"
+    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 }
 /^BEGIN/                  { in_begin=1 }
 in_begin && /^}/          { in_begin=0 }
 in_begin && $1 ~ /^split/ { next }
 { gsub("\\s*#.+$", ""); gsub(Q, Q "\\" Q Q); if (trim($0)) print}' makesure.awk
-    echo \'' Makesurefile "$@"'
+    echo \''$X Makesurefile "$@"'
   } > makesure_stable
 
 @goal default

makesure_stable

@@ -1,5 +1,5 @@
 #!/bin/sh
-command -v gawk >/dev/null && AWK='gawk -ltime -v Gawk=1' || AWK=awk
+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"
@@ -585,4 +585,4 @@ function isDir(path) { return ok("test -d " quoteArg(path)) }
 function rm(f) { system("rm " quoteArg(f)) }
 function quoteArg(a) { gsub("'\''", "'\''\\'\'''\''", a); return "'\''" a "'\''" }
 function trim(s) { sub(/^[ \t\r\n]+/, "", s); sub(/[ \t\r\n]+$/, "", s); return s }
-' Makesurefile "$@"
+'$X Makesurefile "$@"