fixed whitespace for *.sh

This commit is contained in:
stefan-hoeck 2021-01-22 14:55:25 +01:00 committed by G. Allais
parent 721cc3162c
commit 606bc577b5
3 changed files with 9 additions and 9 deletions

View File

@ -41,7 +41,7 @@ while getopts ${optstring} arg; do
chez|refc|racket|gambit)
BACKEND="$2"
export IDRIS2_CG=$BACKEND ;;
*)
*)
echo "$BACKEND is not a recognised backend! You can check the available backends using $0 -h"
exit 1 ;;
esac
@ -49,7 +49,7 @@ while getopts ${optstring} arg; do
# test speed flag
f) FAST=true ;;
# custom output file name
o)
o)
[[ ! -z "$2" ]] && FILENAME="$2"
echo "-o option passed, with value $FILENAME"
;;
@ -67,11 +67,11 @@ done
#begin tests
cwd=$(pwd)
if [ $FILENAME != "bench-results" ];
then
if [ $FILENAME != "bench-results" ];
then
echo here
output_path="$FILENAME.csv";
else
output_path="$FILENAME.csv";
else
output_path="$cwd/${FILENAME}_${BACKEND}"
if [[ $FAST = true ]]; then output_path+="_fast"; fi
output_path+=".csv"
@ -118,4 +118,4 @@ done
echo $dashes
echo "benchmarks complete! data written to $output_path"
# end tests
# end tests

View File

@ -1,6 +1,6 @@
#!/usr/bin/env sh
if [ $OS = "windows" ]; then
MY_PWD="$(cygpath -m $(pwd))\\\\"
MY_PWD="$(cygpath -m $(pwd))\\\\"
else
MY_PWD=$(pwd)/
fi

View File

@ -1,6 +1,6 @@
#!/usr/bin/env sh
if [ $OS = "windows" ]; then
MY_PWD="$(cygpath -m $(pwd))\\\\"
MY_PWD="$(cygpath -m $(pwd))\\\\"
else
MY_PWD=$(pwd)/
fi