--- a/common/bin/shell-tracer.sh	Mon Nov 24 14:44:10 2014 +0100
+++ b/common/bin/shell-tracer.sh	Thu Nov 27 15:41:56 2014 +0100
@@ -26,12 +26,12 @@
 #
 # This shell script is supposed to be set as a replacement for SHELL in make,
 # causing it to be called whenever make wants to execute shell commands.
-# The <shell command line> is suitable for passing on to the old shell, 
+# The <shell command line> is suitable for passing on to the old shell,
 # typically beginning with -c.
 #
-# This script will make sure the shell command line is executed with 
+# This script will make sure the shell command line is executed with
 # OLD_SHELL -x, and it will also store a simple log of the the time it takes to
-# execute the command in the OUTPUT_FILE, using the "time" utility as pointed 
+# execute the command in the OUTPUT_FILE, using the "time" utility as pointed
 # to by TIME_CMD. If TIME_CMD is "-", no timestamp will be stored.
 
 TIME_CMD="$1"