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

chore: update-stage0 output should not depend on locale

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-20 10:35:43 +02:00
parent 3c8400d30f
commit 26dab90b1b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
script/update-stage0
View file

@ -3,7 +3,7 @@ set -euo pipefail
rm -r stage0 || true
mkdir -p stage0/
c_files="$(cd src; find . -name '*.lean' | sed s/.lean/.c/ | sort | tr '\n' ' ')"
c_files="$(cd src; find . -name '*.lean' | sed s/.lean/.c/ | LC_ALL=C sort | tr '\n' ' ')"
for f in $c_files; do mkdir -p $(dirname stage0/stdlib/$f); cp $LIB/temp/$f stage0/stdlib/$f; done
# ensure deterministic ordering
echo "add_library (stage0 OBJECT $c_files)" > stage0/stdlib/CMakeLists.txt