diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-07 10:37:47 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-07 10:37:47 +0100 |
| commit | 2f679ec5235257c9fd106c26c15049e04523a307 (patch) | |
| tree | c7fa324a7e157c7131468cf136f61968c9e1390b /tools | |
| parent | c8f6903de4d9debb3fe38755a3f5e7b558a014e2 (diff) | |
| parent | adbefdb8a9d9e7459630aa1808eae5b42cb3a6a5 (diff) | |
Merge PR #6142: Single quotes break on Windows
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 87783350a..7fd942908 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -172,7 +172,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 | cut -d " " -f 1) COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") |