idris-1.1.0: scripts/runidris

#!/bin/sh

# This is a script that runs an idris program, suitable for use
# in a shebang line. We cache the executables by naming them after
# the SHA hash of the idris source and looking for it before
# compiling
RUNIDRIS_DIR="${TEMP:-/tmp}/runidris"
if [ ! -d $RUNIDRIS_DIR ]; then
    mkdir $RUNIDRIS_DIR
    chmod 700 $RUNIDRIS_DIR
fi
TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`"
FP="$RUNIDRIS_DIR/$TEMP_NAME"
if [ ! -e $FP ]; then
    "${IDRIS:-idris}" $1 --ibcsubdir "$RUNIDRIS_DIR" -i "." -o $FP
fi
shift
"$FP" "$@"