mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 16:51:51 +03:00
a972778eab
They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
21 lines
494 B
Plaintext
Executable File
21 lines
494 B
Plaintext
Executable File
# This test needs to run `idris2` from a sub-folder.
|
|
# Split path to `idris2` executable into dirname and basename.
|
|
# If the path is relative, add `..` to compensate for running `idris2` in a sub-folder.
|
|
case "$1" in
|
|
/*)
|
|
# Absolute path
|
|
IDRIS2_DIR="$(dirname "$1")"
|
|
;;
|
|
*)
|
|
# Relative path
|
|
IDRIS2_DIR="$(dirname "$1")/.."
|
|
;;
|
|
esac
|
|
|
|
IDRIS2_EXEC="$(basename "$1")"
|
|
|
|
cd "folder with spaces" || exit
|
|
|
|
"$IDRIS2_DIR/$IDRIS2_EXEC" --no-banner Main.idr < ../input
|
|
rm -rf build
|