diff options
Diffstat (limited to 'test-suite')
3 files changed, 1 insertions, 21 deletions
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired index 7900c034da..4381160a4e 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -1,15 +1,5 @@ -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' COQDEP VFILES -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' COQC Slow.v Slow (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko) COQC Fast.v Fast (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko) -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired index 7ab0bc75d9..e6af909268 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired @@ -1,15 +1,5 @@ -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' COQDEP VFILES -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' COQC Slow.v Slow (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko) COQC Fast.v Fast (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko) -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 4ee4aae36c..f556638640 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -63,7 +63,7 @@ TO_SED_IN_PER_LINE=( for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do for ext in "" .desired; do - grep -v 'warning: undefined variable' < ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed + sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" ${file}${ext} > ${file}${ext}.processed done echo "cat $file" cat "$file" |