git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/scripts/runidris
18 lines 526 B history raw
1#!/bin/sh
3# This is a script that runs an idris program, suitable for use
4# in a shebang line. We cache the executables by naming them after
5# the SHA hash of the idris source and looking for it before
6# compiling
7RUNIDRIS_DIR="${TEMP:-/tmp}/runidris"
8if [ ! -d $RUNIDRIS_DIR ]; then
9 mkdir $RUNIDRIS_DIR
10 chmod 700 $RUNIDRIS_DIR
11fi
12TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`"
13FP="$RUNIDRIS_DIR/$TEMP_NAME"
14if [ ! -e $FP ]; then
15 "${IDRIS:-idris}" $1 --ibcsubdir "$RUNIDRIS_DIR" -i "." -o $FP
16fi
17shift
18"$FP" "$@"