diff options
| author | Gaëtan Gilbert | 2020-01-06 15:27:05 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-06 15:27:05 +0100 |
| commit | 95124216fba92f75e0aef97f4c0003eeb8689557 (patch) | |
| tree | cd6698fde2a9299c71fb7d0f35322183506cd96f | |
| parent | 793bddef6b4f615297e9f9088cd0b603c56b2014 (diff) | |
| parent | 4541dab0cfc3389dee7440b147108d91a7b32840 (diff) | |
Merge PR #11211: Fixing status reporting for complexity tests
Reviewed-by: SkySkimmer
| -rw-r--r-- | test-suite/Makefile | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index b3a633e528..1d21b4b5e0 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -530,14 +530,16 @@ $(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 | sed "s/\r//g"`; \ + 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); \ echo " $<...Error! (should be accepted)" ; \ + $(FAIL); \ elif [ "$$res" = "" ]; then \ echo $(log_failure); \ echo " $<...Error! (couldn't find a time measure)"; \ + $(FAIL); \ else \ true "express effective time in centiseconds"; \ resorig="$$res"; \ |