diff options
| author | Gaëtan Gilbert | 2020-04-20 13:21:25 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-20 13:21:25 +0200 |
| commit | b669ca8459f5d0fec2201c494d88c7d516c37be0 (patch) | |
| tree | 94f96d958508e1db7e518257c1024d3cb463b12d /test-suite | |
| parent | e77b7aed145718b73ca58c75bc7ed01d2b55446f (diff) | |
| parent | ff293b3564efec8c911c3df9cd3a71863161d8b3 (diff) | |
Merge PR #12125: Fix Makefile warning: undefined variable '*'
Reviewed-by: SkySkimmer
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" |