diff -r cf57e8c78492 -r 86d8bbc99e7b scripts/awk
--- a/scripts/awk	Thu May 23 23:35:52 2019 +0200
+++ b/scripts/awk	Sat May 25 11:36:31 2019 +0200
@@ -47,9 +47,17 @@
 	done | relpipe-in-cli generate-from-stdin args 2 i integer value string | relpipe-out-tabular
 }
 
+realAWK() {
+	/usr/bin/awk "$@"
+	echo "$?" > "$logDir/awk-status.log"
+}
+
 formatArgsTxt "$@" > "$logDir/awk-args.log";
 
-tee "$logDir/awk-stdin.log" | /usr/bin/awk "$@" 2> "$logDir/awk-stderr.log" | tee "$logDir/awk-stdout.log";
+tee "$logDir/awk-stdin.log" | realAWK "$@" 2> "$logDir/awk-stderr.log" | tee "$logDir/awk-stdout.log";
+
+cat "$logDir/awk-stderr.log" >&2;
+exit `cat "$logDir/awk-status.log"`;
 
 # Use e.g. GNU Screen with four windows to watch files:
 # watchFile() { while inotifywait "$1" &>/dev/null ; do clear; cat "$1" ; done; }