diff options
| author | Hugo Herbelin | 2020-02-28 11:41:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-22 15:02:43 +0100 |
| commit | 475650c6425fb3ed91f388db7e7da918950f0194 (patch) | |
| tree | 981d08eca15f956e03419898a39bd9753c8eb18a | |
| parent | 08189431706298d599cffea2e41dd51290305ba3 (diff) | |
Test-suite: Assume coqtop output is text even with non-printable characters.
| -rw-r--r-- | test-suite/Makefile | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 6696f1431e..0d8a6ebed7 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -417,14 +417,16 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ output=$*.out.real; \ + export LC_CTYPE=C; \ + export LANG=C; \ $(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ - | grep -v "Welcome to Coq" \ - | grep -v "\[Loading ML file" \ - | grep -v "Skipping rcfile loading" \ - | grep -v "^<W>" \ + | grep -a -v "Welcome to Coq" \ + | grep -a -v "\[Loading ML file" \ + | grep -a -v "Skipping rcfile loading" \ + | grep -a -v "^<W>" \ | sed 's/File "[^"]*"/File "stdin"/' \ > $$output; \ - diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ + diff -a -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ |