diff options
| author |  Carl Patenaude Poulin <carl.patenaudepoulin@mail.mcgill.ca> | 2017-11-11 15:45:58 -0500 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2017-11-11 15:45:58 -0500 |
| commit | adbefdb8a9d9e7459630aa1808eae5b42cb3a6a5 (patch) | |
| tree | 65a99a66888c246fda2ba943389d0cc10dd13345 /tools | |
| parent | d9f79d97dbc503e149cba2df1b228a94d7ac970b (diff) | |
Single quotes break on Windows
As it is, running a `Makefile.coq` on Windows produces the following error:
`cut: ': No such file or directory`
Changing to double quotes fixes this.
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 8f79f8a66..cb628a05f 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)") |