idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-18 16:51:51 +03:00
Code Issues Projects Releases Wiki Activity

[ fix #3339 ] Set the global test locale

Browse Source
This commit is contained in:
Denis Buzdalov 2024-07-01 19:21:55 +03:00 committed by G. Allais
parent c5abf4be35
commit 22c25e945e
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
tests/testutils.sh
View File

@ -109,6 +109,9 @@ if [ -z "$PREFIX_CHANGED" ] && [ -n "$IDRIS2_PREFIX" ]; then
export PREFIX_CHANGED=1 export PREFIX_CHANGED=1
fi fi
# Set the most neutral locale for reproducibility
export LC_ALL=C.UTF-8
# Remove test directory from output # Remove test directory from output
# Useful for consistency of output between machines # Useful for consistency of output between machines
# Usage: run SomeTest.idr | filter_test_dir # Usage: run SomeTest.idr | filter_test_dir