diff export_local_file.sh @ 0:c772c8912663

Uploaded

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/export_local_file.sh	Tue Feb 28 12:36:45 2012 -0500
@@ -0,0 +1,43 @@
+###
+### The shell script: export_local_file.sh
+###
+### The script basically copies a Galaxy dataset (param 1, dataset_NNNNN.dat) 
+### to the destination file (param 2, {/data,/home}/filename
+###
+#!/bin/sh
+
+INPUT="$1"
+DEST="$2"
+EMAIL="$3"
+OUTPUT="$4"
+USER=`echo $EMAIL | sed -e 's#@.*##'`
+
+if [ -z "$DEST" ]; then
+	echo "Usage: $0 [INPUT] [DEST]" >&2
+	exit 1
+fi
+
+# Filter any unwanted directories
+
+if [[ `echo $DEST | grep -c ^/data/` -lt 1 ]] && [[ `echo $DEST | grep -c ^/home/` -lt 1 ]] ; then
+  echo "Error: \"$DEST\" is not allowed" >&2
+  exit 1
+fi
+
+# Do the deed
+
+cpy $INPUT $DEST "$USER"
+dataset=`basename $INPUT`
+if [ $? != 0  ]; then
+  echo "Error: $USER failed to copy dataset $dataset to \"$DEST\"" >&2 
+  exit 1
+fi
+
+echo "Dataset $dataset successfully exported to \"$DEST\"" >> $OUTPUT
+
+exit 0
+
+###
+###
+###
+