max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(tests/lean/interactive/test_single): MSYS2 compatibility

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-01 11:44:55 -08:00
parent a9daf9390a
commit ffcb9f240e
1 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
tests/lean/interactive/test_single.sh
View file

@ -8,6 +8,15 @@ fi
ulimit -s unlimited
LEAN=$1
ROOT_PATH=$($REALPATH ../../..)
if [[ "$OSTYPE" == "msys" ]]; then
# Windows running MSYS2
# Replace /c/ with c:, and / with \\
ROOT_PATH_NORMALIZED=$(echo $ROOT_PATH | sed 's|^/\([a-z]\)/|\U\1:/|' | sed 's|/|\\\\\\\\|g')
else
ROOT_PATH_NORMALIZED=$ROOT_PATH
fi
export LEAN_PATH=$ROOT_PATH/library:.
if [ $# -ne 3 ]; then
INTERACTIVE=no
@ -19,8 +28,12 @@ echo "-- testing $f"
OUTPUT="$("$LEAN" -j0 -D pp.unicode=true --server < "$f")"
# make paths system-independent
OUTPUT=${OUTPUT//$ROOT_PATH/}
echo "$OUTPUT" > "$f.produced.out"
if [[ "$OSTYPE" == "msys" ]]; then
echo "$OUTPUT" | sed "s|$ROOT_PATH_NORMALIZED||g" | sed 's|\\\\|/|g' > "$f.produced.out"
else
OUTPUT=${OUTPUT//$ROOT_PATH_NORMALIZED/}
echo "$OUTPUT" > "$f.produced.out"
fi
if test -f "$f.expected.out"; then
if diff --ignore-all-space "$f.produced.out" "$f.expected.out"; then