diff options
| author | Jason Gross | 2019-12-19 09:13:48 -0500 |
|---|---|---|
| committer | Jason Gross | 2019-12-19 09:13:48 -0500 |
| commit | 925a87275245fbd1ea5142f02950f89a8b37d19c (patch) | |
| tree | 82e57b7a69bc0fc152309bd6eb797a950bf79e61 | |
| parent | baab1c01b22d754df64a09be436d350663cc1c28 (diff) | |
Remove trailing \r in complexity measures for Windows
| -rw-r--r-- | test-suite/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 1546b7cf62..b3a633e528 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -530,7 +530,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ true "extract effective user time"; \ - res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \ + res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1 | sed "s/\r//g"`; \ R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ |