diff -r b9baecff0684 -r 04d0083cb9e5 Admin/lib/Tools/churn_pie
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/churn_pie	Sat Apr 05 10:03:04 2014 +0200
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+#
+# Author: Florian Haftmann, TU Muenchen
+#
+# DESCRIPTION: pie chart with mercurial churn statistics for specified aliases file
+
+ALIAS="${1:-$ISABELLE_HOME/Admin/user-aliases}"
+shift
+
+SCRIPT="$ISABELLE_HOME/Admin/lib/scripts/churn_pie"
+
+cd "$(dirname "$ALIAS")"
+
+hg churn --aliases "$ALIAS" | "$SCRIPT" "$@"