From 15d61838d7435b45559d648bcde1ccfb6e468bcd Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 7 Jun 2017 15:54:37 -0400
Subject: Fix `make TIMED=1` garbage

It should not emit ` (user: 0.00 mem: 2852 ko)` multiple times---
 tools/CoqMakefile.in | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index bf0669578d..f3a645a21e 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -132,7 +132,7 @@ COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML)
 
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
-COQ_VERSION:=$(shell $(COQC) --print-version | cut -d ' ' -f 1)
+COQ_VERSION:=$(shell $(COQC) --print-version 2>/dev/null | cut -d ' ' -f 1)
 COQMAKEFILE_VERSION:=@COQ_VERSION@
 
 COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
-- 
cgit v1.2.3