--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tools/remove_num_prefix	Wed Oct 15 23:28:56 2008 +0200
@@ -0,0 +1,30 @@
+#!/bin/sh
+
+# Remove a numeric prefix (ex 0010_filename -> filename) on files 
+
+# (c) 2005 Jérôme SAUTRET <jerome@sautret.org>
+# This script is distributed under GNU GPL. Ask Stallman for details.
+
+# $Id: remove_num_prefix,v 1.1 2005/08/22 19:58:27 jerome Exp $
+
+set -o errexit
+if [ -z "$1" ] ; then
+	cat <<EoF
+Usage:
+`basename $0` files...
+Remove a numeric prefix (ex 0010_filename -> filename) on files.
+EoF
+	exit 1
+fi
+
+
+files="$@"
+
+
+i=$min
+for file in $files
+do
+    new="`echo "$file" | sed 's/^0*[0-9][0-9]*_\(.*\)$/\1/'`"
+    echo "$file -> $new"
+    mv "$file" "$new"
+done
\ No newline at end of file