From 70f1d999ff030d20d10f23bcbf95f37216e182c9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 13 Feb 2018 17:24:12 -0500
Subject: Fix issue with spurious timing test failures

When none of the numbers get over 100, the width of the table was
different.

See https://github.com/coq/coq/pull/6736#issuecomment-365386802
---
 test-suite/coq-makefile/timing/run.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 2439d3f378..dfcc31569c 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -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' | 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' | sed s'/+/-/g' | sort > ${file}${ext}.processed
     done
 done
 for file in A.v.timing.diff; do
-- 
cgit v1.2.3