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

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

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/Makesurefile b/Makesurefile
@@ -134,6 +134,7 @@ function trim(s) { sub(/^[ \t\r\n]+/, "", s); sub(/[ \t\r\n]+$/, "", s); return
 /^BEGIN/                  { in_begin=1 }
 in_begin && /^}/          { in_begin=0 }
 in_begin && $1 ~ /^split/ { next }
+/^function gettimeofday/  { next }
 { gsub("\\s*#.+$", ""); gsub(Q, Q "\\" Q Q); if (trim($0)) print}' makesure.awk
     echo \''"$X" Makesurefile "$@"'
   } > makesure_stable

diff --git a/makesure.awk b/makesure.awk
@@ -708,3 +708,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 }
+function gettimeofday(){} # hack for mawk