From 26dab90b1b06a81be2bd59718d16944dd6898ea7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 20 May 2020 10:35:43 +0200
Subject: [PATCH] chore: update-stage0 output should not depend on locale

---
 script/update-stage0 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/script/update-stage0 b/script/update-stage0
index d816180a1e..9132a031da 100755
--- a/script/update-stage0
+++ b/script/update-stage0
@@ -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