comparison common/bin/shell-tracer.sh @ 1475:2b07cd3f89aa

Merge
author asaha
date Mon, 06 Apr 2015 12:13:27 -0700
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:dc95c029daa3
1 #!/bin/bash
2 #
3 # Copyright (c) 2012, Oracle and/or its affiliates. All rights reserved.
4 # DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.
5 #
6 # This code is free software; you can redistribute it and/or modify it
7 # under the terms of the GNU General Public License version 2 only, as
8 # published by the Free Software Foundation.
9 #
10 # This code is distributed in the hope that it will be useful, but WITHOUT
11 # ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
12 # FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
13 # version 2 for more details (a copy is included in the LICENSE file that
14 # accompanied this code).
15 #
16 # You should have received a copy of the GNU General Public License version
17 # 2 along with this work; if not, write to the Free Software Foundation,
18 # Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.
19 #
20 # Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA
21 # or visit www.oracle.com if you need additional information or have any
22 # questions.
23 #
24
25 # Usage: sh shell-tracer.sh <TIME_CMD> <OUTPUT_FILE> <OLD_SHELL> <shell command line>
26 #
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.
29 # The <shell command line> is suitable for passing on to the old shell,
30 # typically beginning with -c.
31 #
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
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.
36
37 TIME_CMD="$1"
38 OUTPUT_FILE="$2"
39 OLD_SHELL="$3"
40 shift
41 shift
42 shift
43 if [ "$TIME_CMD" != "-" ]; then
44 "$TIME_CMD" -f "[TIME:%E] $*" -a -o "$OUTPUT_FILE" "$OLD_SHELL" -x "$@"
45 else
46 "$OLD_SHELL" -x "$@"
47 fi