diff options
| author | Enrico Tassi | 2019-02-22 20:52:14 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-02-22 20:52:14 +0100 |
| commit | dea9f08178efcf9cfac7ee2970dc21abc2fde308 (patch) | |
| tree | 515a3caec0fd881b71ac1cdbab743cfb5fd473bf /Makefile.build | |
| parent | 6a289e4fbc1c4327429bb7041e8f39a18bbb0f70 (diff) | |
| parent | e8419bac30ab98527ec6b15d5a0f5c1035539ca5 (diff) | |
Merge PR #9576: [library] Remove `-boot` option.
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 2b401cd9e6..ea356d5f8e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -201,7 +201,7 @@ COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS) # Beware this depends on the makefile being in a particular dir, we # should pass an absolute path here but windows is tricky # c.f. https://github.com/coq/coq/pull/9560 -BOOTCOQC=$(TIMER) $(COQC) -coqlib . -boot $(COQOPTS) +BOOTCOQC=$(TIMER) $(COQC) -coqlib . -q $(COQOPTS) LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) MLINCLUDES=$(LOCALINCLUDES) |