aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-08 12:45:53 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-08 12:45:53 +0100
commitbd7e7ccf8d60a2c5bf2e53ebe88bde99e291ce07 (patch)
tree5a2f81f171772961442f23391658f5c34e18e89c
parent02f96d47c46a36995444aa46e7dc48c6016fc614 (diff)
parentfbb0ffb8d7cf5055598f8fec01ab55ea74295b88 (diff)
Merge PR #6517: Trim more trailing whitespace in coq-makefile timing test
-rwxr-xr-xtest-suite/coq-makefile/timing/run.sh4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 898af5590..58cda7ada 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -40,7 +40,7 @@ INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected
for ext in "" .desired; do
for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
- cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed
+ cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed
done
done
for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
@@ -74,7 +74,7 @@ echo
for ext in "" .desired; do
for file in A.v.timing.diff; do
- cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/+/-/g' | sort > ${file}${ext}.processed
+ cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/ *$//g' | sed s'/+/-/g' | sort > ${file}${ext}.processed
done
done
for file in A.v.timing.diff; do