diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2017-06-07 15:54:37 -0400 |
|---|---|---|
| committer |  Jason Gross <jgross@mit.edu> | 2017-06-15 16:37:56 -0400 |
| commit | 15d61838d7435b45559d648bcde1ccfb6e468bcd (patch) | |
| tree | 295aba6e5c5403814bf7859c120c608851e0ebe0 /tools | |
| parent | da62d0dd86fc140ff58d9366a7a85e9b21b104b9 (diff) | |
Fix `make TIMED=1` garbage
It should not emit ` (user: 0.00 mem: 2852 ko)` multiple times
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index bf0669578..f3a645a21 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)") |