Index: tools/PrettyGitLogs.sh
===================================================================
--- tools/PrettyGitLogs.sh	(revision 6716d7836e0b9ad9ef228067f20cf7f185f2532f)
+++ 	(revision )
@@ -1,29 +1,0 @@
-#!/bin/bash
-
-set -e
-
-GIT="git --git-dir=$1/.git"
-
-GIT_UPDATE="$2/GIT_UPDATE"
-GIT_LOG="$2/GIT_LOG"
-GIT_DIFF="$2/GIT_DIFF"
-
-rm -f ${GIT_UPDATE}  ${GIT_LOG}  ${GIT_DIFF}
-
-GitOldRef=$3
-GitNewRef=$4
-
-
-revisions=$(git rev-list ${GitOldRef}..${GitNewRef})
-
-for rev in ${revisions}; do
-    type=$(git cat-file -t ${rev})
-    echo "       via  ${rev} (${type})" >>  ${GIT_UPDATE}
-done
-rev=${GitOldRef}
-type=$(git cat-file -t ${rev})
-echo "      from  ${rev} (${type})" >>  ${GIT_UPDATE}
-
-git rev-list --format=short ${GitOldRef}...${GitNewRef} >  ${GIT_LOG}
-
-git diff --stat --color ${GitNewRef} ${GitOldRef} | sed -e 's/\[32m/<span style\=\"color\: \#00AA00\;\">/g' -e 's/\[31m/<span style\=\"color\: \#AA0000\;\">/g' -e 's/\[m/<\/span>/g' >  ${GIT_DIFF}