diff options
| author | Pierre-Marie Pédrot | 2017-09-01 19:11:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-22 15:19:15 +0200 |
| commit | 94b8e1276f6be454e09437faba49564836986a61 (patch) | |
| tree | 961ab7196729040e37edf0ecf46d64f00da184b0 | |
| 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.
| -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 803fe8029a..c4bd11c57d 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 |