diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-01 19:11:05 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-22 15:19:15 +0200 |
commit | 94b8e1276f6be454e09437faba49564836986a61 (patch) | |
tree | 961ab7196729040e37edf0ecf46d64f00da184b0 /test-suite/coq-makefile/template | |
parent | 296941dc97d53817cc58b4687ed99168e1dd33a9 (diff) |
Make a test for coq_makefile portable.
The validity of this test depended on Makefile issueing warnings in English.
We simply force the global language of the shell to be C.
Diffstat (limited to 'test-suite/coq-makefile/template')
-rwxr-xr-x | test-suite/coq-makefile/template/init.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index 803fe8029..c4bd11c57 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -2,6 +2,7 @@ set -e set -o pipefail export PATH=$COQBIN:$PATH +export LC_ALL=C rm -rf theories src Makefile Makefile.conf tmp git clean -dfx || true |