diff --git a/scripts/dist-git/remove_unused_sources b/scripts/dist-git/remove_unused_sources index 0e0cd80..1ff1c52 100755 --- a/scripts/dist-git/remove_unused_sources +++ b/scripts/dist-git/remove_unused_sources @@ -15,7 +15,7 @@ die() { echo "$*" 1>&2 ; exit 1; } logcmd () { - echo >&2 "$*" + echo >&2 "[PID$$:DATE:$(date +"%Y%m%d_%H%M%S")] $*" "$@" }