equal
deleted
inserted
replaced
24 |
24 |
25 # Usage: sh shell-tracer.sh <TIME_CMD> <OUTPUT_FILE> <OLD_SHELL> <shell command line> |
25 # Usage: sh shell-tracer.sh <TIME_CMD> <OUTPUT_FILE> <OLD_SHELL> <shell command line> |
26 # |
26 # |
27 # This shell script is supposed to be set as a replacement for SHELL in make, |
27 # This shell script is supposed to be set as a replacement for SHELL in make, |
28 # causing it to be called whenever make wants to execute shell commands. |
28 # causing it to be called whenever make wants to execute shell commands. |
29 # The <shell command line> is suitable for passing on to the old shell, |
29 # The <shell command line> is suitable for passing on to the old shell, |
30 # typically beginning with -c. |
30 # typically beginning with -c. |
31 # |
31 # |
32 # This script will make sure the shell command line is executed with |
32 # This script will make sure the shell command line is executed with |
33 # OLD_SHELL -x, and it will also store a simple log of the the time it takes to |
33 # OLD_SHELL -x, and it will also store a simple log of the the time it takes to |
34 # execute the command in the OUTPUT_FILE, using the "time" utility as pointed |
34 # execute the command in the OUTPUT_FILE, using the "time" utility as pointed |
35 # to by TIME_CMD. If TIME_CMD is "-", no timestamp will be stored. |
35 # to by TIME_CMD. If TIME_CMD is "-", no timestamp will be stored. |
36 |
36 |
37 TIME_CMD="$1" |
37 TIME_CMD="$1" |
38 OUTPUT_FILE="$2" |
38 OUTPUT_FILE="$2" |
39 OLD_SHELL="$3" |
39 OLD_SHELL="$3" |