From 5bbf1702136b71556a0b3d802702eb6f09813438 Mon Sep 17 00:00:00 2001 From: vanhofen Date: Tue, 6 Aug 2019 21:55:16 +0200 Subject: [PATCH] - add makelog script; based on makelog by max_10 --- makelog | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100755 makelog diff --git a/makelog b/makelog new file mode 100755 index 00000000..cf660607 --- /dev/null +++ b/makelog @@ -0,0 +1,19 @@ +#!/bin/bash + +# makelog - Redirect make's output into logfile + +usage() { + echo "Usage: makelog ..." +} + +test "$1" == "--help" && { usage; exit 0; } +test -z "$1" && { usage; exit 1; } + +logfile=$(mktemp makelog.XXXXXX) +trap "rm -f $logfile" EXIT + +time make S=1 $* 2>&1 | tee $logfile + +mkdir -p build_tmp +echo -e "\nmake $*:\n" >> build_tmp/make.log +cat $logfile >> build_tmp/make.log